An Open Framework for Foundational Proof-Carrying Code Xinyu Feng Yale University Joint work with Zhaozhong Ni (Yale,now at MSR) Zhong Shao (Yale)and Yu GUo (USTC)
An Open Framework for Foundational Proof-Carrying Code Xinyu Feng Yale University Joint work with Zhaozhong Ni (Yale, now at MSR), Zhong Shao (Yale) and Yu Guo (USTC)
Motivation How to build fully certified software systems? Source-level code + Libraries and runtime References with weak upd. Garbage collectors Dynamic mem.alloc. malloc()(strong update) Functions,exceptions,... Stacks,code pointers Concurrency Context switching Scheduler /0 Device drivers
Motivation How to build fully certified software systems? Source-level code + Libraries and runtime References with weak upd. Dynamic mem. alloc. Functions, exceptions, … Concurrency I/O Garbage collectors malloc() (strong update) Stacks, code pointers Context switching & Scheduler Device drivers
Motivation [Yu&Shao,ICFP'04] ■ All concurrency verification {A,G} {A.,G)} assumes built-in concurrency Assume-Guarantee(A-G)reasoning C C R Concurrent Separation logic (CSL) pCa 工 0- 工 H 0 Context switching,scheduler pe Too low-level to be certified in these logics R T T Threads schedulers have never H been modularly certified! TQ
Motivation ◼ All concurrency verification assumes built-in concurrency ◼ Assume-Guarantee (A-G) reasoning ◼ Concurrent Separation logic (CSL) ◼ … ◼ Context switching, scheduler ◼ Too low-level to be certified in these logics [Yu&Shao, ICFP’04] H C R 1 pc1 T1 {(A1 , G1)} Cn pcn Tn {(An, Gn)} i . . . H R C1 Cn . . . . . . CS pc ctxt1 ctxtn TQ ◼ Threads & schedulers have never been modularly certified!
Motivation Certify all code in a single type system/program logic? Hard to combine all features weak vs.strong update,functions/exceptions vs.goto's,threads vs. thread contexts May not be modular Very complex,hard to use Don't know how to design such a logic Certify modules using the most appropriate logic! Modules do not use all the features at the same time It is simpler to use specialized logic for each module
Motivation ◼ Certify all code in a single type system/program logic? ◼ Hard to combine all features ◼ weak vs. strong update, functions/exceptions vs. goto’s, threads vs. thread contexts ◼ May not be modular ◼ Very complex, hard to use ◼ Don’t know how to design such a logic ◼ Certify modules using the most appropriate logic! ◼ Modules do not use all the features at the same time ◼ It is simpler to use specialized logic for each module
An Open Framework Certify different modules using different verification systems! Proof of SP C 平1HC Ck 平卢C 9 凸C2平2
An Open Framework Certify different modules using different verification systems! Proof of SP C1 C2 C1 L1 k Ck Lk Ck C1 C C2 Ck ... C2: L2
Challenges Extensibility and openness not designed for certain specific interoperations But can we just use MLFs, e.g.Coq? Expressiveness type safety,concurrency properties,partial correctness,.. A general and uniform model of control flow Allow functions certified in different systems to call each other the key for modularity:separate verification proof reuse Principled interoperation with clear meta-property properties of the whole system composed of modules Not readily supported in Coq!
Challenges ◼ Extensibility and openness ◼ not designed for certain specific interoperations But can we just use MLFs, e.g. Coq? ◼ Expressiveness ◼ type safety, concurrency properties, partial correctness, … ◼ A general and uniform model of control flow ◼ Allow functions certified in different systems to call each other ◼ the key for modularity: separate verification & proof reuse ◼ Principled interoperation with clear meta-property ◼ properties of the whole system composed of modules Not readily supported in Coq!
Our contributions OCAP:an open framework Embedding of different systems TAL,non-CPS Hoare-logic,A-G reasoning,.. ■Open&Extensible Modularity with first-class code pointers [Ni&shao POPL06] ■Soundness Type safety,preservation of invariants in foreign systems ▣Applications TAL memory allocation libs. Threads Scheduler The first time to modularly certify both sides ■
Our contributions ◼ OCAP: an open framework ◼ Embedding of different systems ◼ TAL, non-CPS Hoare-logic, A-G reasoning, … ◼ Open & Extensible ◼ Modularity with first-class code pointers [Ni&Shao POPL’06] ◼ Soundness ◼ Type safety, & preservation of invariants in foreign systems ◼ Applications ◼ TAL + memory allocation libs. ◼ Threads + Scheduler ◼ The first time to modularly certify both sides ◼ …
Outline ■OCAP Framework Certifying Threads Schedulers
Outline ◼ OCAP Framework ◼ Certifying Threads & Schedulers
OCAP:Overview ! C1 …2 Cn L1 Cr [o on Sound Sound [on OCAP Rules OCAP Soundness Modeling of the machine TCB Mechanized Meta-Logic(CiC)
OCAP Rules … Ln OCAP : Overview OCAP Soundness Mechanized Meta-Logic (CiC) Modeling of the machine TCB Sound L1 ( )L1 ( )Ln Sound Mechanized Meta-Logic (CiC) Modeling of the machine … C1 Cn
The Machine (data heap) f 工1 pc addu f2: 2 0 12 lw … SW fa: 工3 ￥1 r2 r3 jf (register file)R (code heap)c (state)s:=(H,R) (instr.seq.)I ::={f→工}* (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