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 stackbased 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 !