second,the primary inference rules are based on the oper- of the proof. ational semantics of the instructions,that is,the machine The precondition p of the basic block is state before the execution of an instruction is used to calcu- late the state after it [12].While in Hoare logic,the calcu- AS.S(S(ebp)-16)=S(S(ebp)+16)x S(S(ebp)-20)A lation of the precondition from the postcondition is directly S(S(ebp)-20)<S(S(ebp)+12)A based on syntactic substitution.Generally,machine state S(S(ebp)-20)<S(S(ebp)+12). denotes a map from registers,stack locations and heap loca- tions to values.The change of machine state is based on the (Note that the corresponding assertion at source level is operational semantics of the instructions.The formal de- {x=m*yAy<=n∧y<n}) scription of our proof-carrying assembly code has referred The postcondition g(g is also the precondition of the to CAP and SCAP [19,6],which are common frameworks succeeding basic block 1loop)is supporting Hoare style reasoning for assembly code certifi- cation. AS.S(S(ebp)-16)=S(S(ebp)+16)x S(S(ebp)-20)A The instruction execution may change pointer informa- S(S(ebp)-20)<S(S(ebp)+12). tion in II,N and D,and the change can be deduced ac- cording to the pointer logic at assembly level [11].Besides (Similarly,the corresponding assertion at source level is function call,the instructions which may change the pointer {x ==m y ay <n},i.e.,the loop invariant.) information include mov1,pushl etc.(we call them assign- In these assertions,S denotes the current machine state. ment instructions in general).The rules for these instruc- If the postcondition of an instructiont is Q,its precondition tions in the pointer logic at assembly level are almost the P can be achieved through the formula:(note that P and Q same as the corresponding assignment rules at source level, are parameterized by a machine state S) except that variables are replaced by memory addresses, registers,and register indirect addresses etc.Since there P=gp(L,Q)=AS.Q(upd(S,)) is no complex access path in assembly programs,aliasing calculation at assembly level is much simpler than that at where the function upd(S,)represents the operational se- source level. mantics of the instruction t,and the return value of upd(S, is a machine state after the execution of the instruction t in To generate the proof of a basic block satisfying its pre- state S. and postconditions,it is important to generate assertions Figure 5 shows the operational semantics and precondi- between the instructions in the basic block.These asser- tion generation formulas of some instructions.Sab is tions can be generated from the pre-and postconditions of a machine state,and it means: the basic block.According to P,Q and the correspond- ing machine state,the verification framework at assembly b ifc=a, level checks whether P}O}holds for each instruction Sa→(c)= S(c)ifc≠a. t in the basic block.Pointer-related assertions are generated and inserted into the basic block in a forward manner,with For example,suppose the postcondition for instruction integer-related assertions in a backward manner.Pointer- “mov1r1,r2”is related assertions at assembly level are rather difficult to understand,so we take a basic block with integer-related λS.S(r2)=3, assertions as an example to explain how to generate and in- according to gp((movl r1,r2),Q)in Figure 5,the pre- sert assertions between instructions. condition is The source program in Figure 4 is a function to mul- tiply integer m by n.The assertions in notation {are λS.(S'.S'(r2)=3)Sr2→S(r1)): provided by programmers.The precondition of the func- tion is represented as the assertion in the first line;in line that is, 12 is the postcondition.The loop invariant for while is in λS.S[r2→S(r1)](r2)=3. line 6.The symbol"result"represents the return value According to the definition of Slab],the precondition of the function.The assembly code in the same figure cor- can be reduced to responds to the while loop (line 6-9).where the addresses of n,m,x and y in the stack are represented by 12(%ebp), λS.S(r1)=3. 16(%ebp),-16(%ebp)and -20(%ebp)respectively,and ebp is the base pointer of current stack frame.Then,we take the basic block Itrue(the basic block which are num- Using gp(,Q),we can get the precondition of each bered in Figure 4)as an example to explain the generation instruction backward from the postcondition of the basicsecond, the primary inference rules are based on the oper￾ational semantics of the instructions, that is, the machine state before the execution of an instruction is used to calcu￾late the state after it [12]. While in Hoare logic, the calcu￾lation of the precondition from the postcondition is directly based on syntactic substitution. Generally, machine state denotes a map from registers, stack locations and heap loca￾tions to values. The change of machine state is based on the operational semantics of the instructions. The formal de￾scription of our proof-carrying assembly code has referred to CAP and SCAP [19, 6], which are common frameworks supporting Hoare style reasoning for assembly code certifi- cation. The instruction execution may change pointer informa￾tion in Π, N and D, and the change can be deduced ac￾cording to the pointer logic at assembly level [11]. Besides function call, the instructions which may change the pointer information include movl, pushl etc. (we call them assign￾ment instructions in general). The rules for these instruc￾tions in the pointer logic at assembly level are almost the same as the corresponding assignment rules at source level, except that variables are replaced by memory addresses, registers, and register indirect addresses etc. Since there is no complex access path in assembly programs, aliasing calculation at assembly level is much simpler than that at source level. To generate the proof of a basic block satisfying its pre￾and postconditions, it is important to generate assertions between the instructions in the basic block. These asser￾tions can be generated from the pre- and postconditions of the basic block. According to P, Q and the correspond￾ing machine state, the verification framework at assembly level checks whether {{P}} ι {{Q}} holds for each instruction ι in the basic block. Pointer-related assertions are generated and inserted into the basic block in a forward manner, with integer-related assertions in a backward manner. Pointer￾related assertions at assembly level are rather difficult to understand, so we take a basic block with integer-related assertions as an example to explain how to generate and in￾sert assertions between instructions. The source program in Figure 4 is a function to mul￾tiply integer m by n. The assertions in notation {{ }} are provided by programmers. The precondition of the func￾tion is represented as the assertion in the first line; in line 12 is the postcondition. The loop invariant for while is in line 6. The symbol “result” represents the return value of the function. The assembly code in the same figure cor￾responds to the while loop (line 6-9), where the addresses of n, m, x and y in the stack are represented by 12(%ebp), 16(%ebp), -16(%ebp) and -20(%ebp) respectively, and ebp is the base pointer of current stack frame. Then, we take the basic block ltrue (the basic block which are num￾bered in Figure 4) as an example to explain the generation of the proof. The precondition p of the basic block is λS.S(S(ebp) − 16) = S(S(ebp) + 16) × S(S(ebp) − 20)∧ S(S(ebp) − 20) ≤ S(S(ebp) + 12)∧ S(S(ebp) − 20) < S(S(ebp) + 12). (Note that the corresponding assertion at source level is {{x == m * y ∧ y <= n ∧ y < n}}.) The postcondition q (q is also the precondition of the succeeding basic block lloop) is λS.S(S(ebp) − 16) = S(S(ebp) + 16) × S(S(ebp) − 20)∧ S(S(ebp) − 20) ≤ S(S(ebp) + 12). (Similarly, the corresponding assertion at source level is {{x == m * y ∧ y <= n}}, i.e., the loop invariant.) In these assertions, S denotes the current machine state. If the postcondition of an instruction ι is Q, its precondition P can be achieved through the formula: (note that P and Q are parameterized by a machine state S) P = gp(ι, Q) = λS.Q (upd(S, ι)), where the function upd(S, ι) represents the operational se￾mantics of the instruction ι, and the return value of upd(S, ι) is a machine state after the execution of the instruction ι in state S. Figure 5 shows the operational semantics and precondi￾tion generation formulas of some instructions. S[a → b] is a machine state, and it means: S[a → b](c) =
b if c = a, S(c) if c = a. For example, suppose the postcondition for instruction “movl r1, r2” is λS.S(r2)=3, according to gp((movl r1, r2), Q) in Figure 5, the pre￾condition is λS.((λS
.S
(r2) = 3) S[r2 → S(r1)]), that is, λS.S[r2 → S(r1)](r2)=3. According to the definition of S[a → b], the precondition can be reduced to λS.S(r1)=3. Using gp(ι, Q), we can get the precondition of each instruction backward from the postcondition of the basic