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