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}*