《计算机科学》相关教学资源（PPT课件讲稿）Modular Verification of Assembly Code with Stack-Based Control Abstractions

Modular Verification of Assembly Code with Stack-Based Control Abstractions Xinyu Feng Yale University Joint work with Zhong Shao,Alexander Vaynberg, Sen Xiang and Zhaozhong Ni

Modular Verification of Assembly Code with Stack-Based Control Abstractions Xinyu Feng Yale University Joint work with Zhong Shao, Alexander Vaynberg, Sen Xiang and Zhaozhong Ni

Motivation How to verify the safety correctness properties of low-level system software? System Java (JML) C#(Spec # Software Cyclone CCured TAL Vanilla CC++&Assembly? Hardware

Motivation How to verify the safety & correctness properties of low-level system software? Vanilla C & C++ & Assembly? Hardware Java (JML) C# (Spec #) Cyclone CCured TAL System … Software

Verifying C&Assembly? Many challenges .. This talk:how to specify/verify low-level stack- based control flows? How to formulate the stack invariants? How to design a compositional program logic? Previous work does not apply! Hoare-Logic done at high-level:no explicit stacks! TAL Proof-Carrying Code: Mostly use continuations CPS-based reasoning Too general to distinguish different stack abstractions

Verifying C & Assembly? Many challenges … This talk: how to specify/verify low-level stack￾based control flows? ◼ How to formulate the stack invariants? ◼ How to design a compositional program logic? Previous work does not apply! ◼ Hoare-Logic done at high-level: no explicit stacks! ◼ TAL & Proof-Carrying Code: ◼ Mostly use continuations & CPS-based reasoning ◼ Too general to distinguish different stack abstractions

Problems -call/return void f(){ void h(){ h(): return; Stacks are hidden! return; } f: pc sw Sra,-4($fp) h: jal h ;；$ra contains ct pc→ ct:1w Sra,-4($fp) +pc jr Sra jr Sra Does f use the right return addr.?

Problems – call/return void f(){ void h(){ h(); return; return; } } f: ... sw $ra, -4($fp) h: jal h ;; $ra contains ct ct: lw $ra, -4($fp) jr $ra ... jr $ra Stacks are hidden! Does f use the right return addr.? pc pc pc

Problems-setjmp/longjmp jmp buf e env=...; void cmp0 (int x,jmp buf env){ int rev(int x){fo pc cmp1(x,env); f pcif (setjmp (env)==0){ cmpO(x,env）: env cannot outlive the stack frame of rev Jelse[ oI env return 1; 6 longjmp(env,1); else return i sp→

f2 … f1 … Problems – setjmp/longjmp int rev(int x){ if (setjmp(env) == 0){ cmp0(x, env); return 0; }else{ return 1; } } void cmp0(int x,jmp_buf env){ cmp1(x, env); } void cmp1(int x,jmp_buf env){ if (x == 0) longjmp(env, 1); else return; } jmp_buf env = …; pc f0 … sp env f0 f1 pc pc f2 env cannot outlive the stack frame of rev !

Our Contributions A simple program logic (SCAP)for modular verification of (1)compiled C code &(2)manually-written assembly code Stack-Based Reasoning Definition Control Abstraction System Formalization function call/return SCAP SEC 4 tail call optimization [34,8] SCAP SEC 4.3 All systems are lemma libraries built on a single CAPO framework! multi-return function call [32] SCAP-II SEC 5.2 weak continuation [30] SCAP-IΠ SEC 5.2 setjmp/longjmp [20] SCAP-II SEC 5.3 coroutines [10] CAP-CR SEC 6.1 coroutines function call [10] SCAP-CR SEC 6.2 threads [15] FCCAP TR [13]

No ’s! Our Contributions A simple program logic (SCAP) for modular verification of (1) compiled C code & (2) manually-written assembly code All systems are lemma libraries built on a single CAP0 framework!

Outline of This Talk Motivations and contributions SCAP logic for verifying function call/return 。Basic framework ■Specifications ■Stack-invariant Instruction rules(to enforce the invariant) Generalizations for complicated controls Implementation applications

Outline of This Talk ◼ Motivations and contributions ◼ SCAP logic for verifying function call/return ◼ Basic framework ◼ Specifications ◼ Stack-invariant ◼ Instruction rules (to enforce the invariant) ◼ Generalizations for complicated controls ◼ Implementation & applications

The Machine (data heap) 工1 pc addu f2: 2 0 12 lw SW... fa: 工3 r2 r3 jf (register file)R (code heap)c (state)s:=(H,R) (instr.seq.)I ::={f→I}* (program)P:=(c,s,pc)

The Machine I1 f1: I2 f2: I3 f3: … (code heap) C 0 r1 1 2 … r2 r3 … rn (data heap) H (register file) R (state) S addu … lw … sw … … j f (instr. seq.) I (program) P::=(C,S,pc) ::=(H,R) ::={f  I}* pc

Invariant-Based Verification 90 C1 C2 S2 C3 6 Initial condition:Inv(So) Progress: if Inv(s),then 3s'.ss. Preservation: if Inv(s)and s s',then Inv (S')

Invariant-Based Verification Initial condition: Inv(S0) S0 c1 S1 c2 S2 c3 … cn Sn Progress: if Inv(S), then S’. S c S’. Preservation: if Inv(S) and S c S’, then Inv(S’)

Program Specifications (spec)平：：={f+a]* (data heap) f1: a2 pc addu f 12 012 1w SW a3 f3: 3 r1 ￥2 r3 In jf (register file)R (code heap)c (state)s:=(H,R) (instr.seq.)I ::={f→I}* (program)P:=(c,s,pc)

Program Specifications I1 f1: I2 f2: I3 f3: … (code heap) C 0 r1 1 2 … r2 r3 … rn (data heap) H (register file) R (state) S addu … lw … sw … … j f (instr. seq.) I (program) P::=(C,S,pc) ::=(H,R) ::={f  I}* pc a1 a2 a3 (spec)  ::= {f  a}*