Certifying Assembly Programs Using A Control-flow-explicit Language

With regard to the critical demand on the safety and correctness of systemsoftwares and executable codes from the computer programmers and users, pro-gram certifcation has been very popular in the computer science research area,since it is able to ensure the high accuracy and reliability of its result. Certifyinga program means that providing a mechanized mathematical proof showing thatthe program satisfes some user-concerned properties, which are expressed with itsspecifcation. In recent decades, in order to make the safety and correctness of pro-grams independent of the large and complex compilers, more and more certifyingworks choose to certify programs directly over assembly languages.Assembly programs are, however, hard to reason about, since the programabstractions (for example, while loop blocks and functions) that one can rely on inhigh-level languages are not structured. The only structure in assembly programsis the basic code block, which is a sequence of instructions ending with a jumpor an indirect jump. Previous program logics for certifying assembly programssupport diferent abstractions mainly by viewing the programs in Continuation-Passing Style (CPS). CPS certifying systems treat the basic code block as thebasic module and totally ignore the program abstractions, which makes them veryhard to certify large softwares. Furthermore, CPS program logics are mainly forthe basic safety property of assembly programs, but not the partial correctnessproperty, which is not only for the safety but also the correctness of the programs.In this dissertation, we propose solutions to the above issues. The maincontents and contributions are as following:We present a brand new methodology of certifying assembly programs, whichmakes it possible to reason about the partial correctness property of assem-bly programs without losing the understanding of any program abstraction-s. When reasoning an assembly program, previous programs logics directlywrite specifcations based on the real code and then reason about the programwith their inference rules. In this dissertation, we introduce an intermediateauxiliary structure, which is a control-fow-explicit language CFEL, between the the specifcation and the real code. We use CFEL to illustrate the con-trol fow of the program execution and use the control fow to represent theactual program during the certifying process. CFEL is simple but power-ful enough to illustrate the control fow of diferent kinds of abstractionsincluding function call/return, exception handling, embedded code pointersand self-modifying code. Before a program is certifed, we frst use CFEL toillustrate the control fow of it to help the certifcation and the specifcationswill be written based on the CFEL structures.Based on CFEL, we give a simple, modular and general program logic sys-tem TCAP to reason about the partial correctness property. The rules inTCAP guarantee that the control fows are correctly illustrated in CFELand well specifed by their corresponding specifcations. Assembly program-s with diferent program abstractions can be certifed in one logic system.Even though TCAP is powerful, it is also clean and easy to use since thespecifcations and rules do not need to worry about as much control fow asbefore, thanks to CFEL. Some non-trivial examples of using TCAP to certifyreal programs are provided.An step-index based semantic model is provided to explain specifcations andjudgements in TCAP and the soundness of the logic system TCAP is provenin a totally semantical fashion. The step-index denotes how many steps ofsafe execution the current program cares. Providing a semantic model to alogic system with diferent program abstractions is not easy. Many assembly-level logic systems have to prove their soundness syntactically. Giving asemantic model to a logic system can makes it easier to be extended with themeanings of its inference rules. The Modularity and genericity are anotherbenefts of the semantic methods. We also show that our semantic modelcan be extended and used to explain the high-order frame rule, which is oneof the most difcult issues in local reasoning area.