《AnOpenFrameworkforFoundationalProofCarryingCode》由会员分享，可在线阅读，更多相关《AnOpenFrameworkforFoundationalProofCarryingCode（29页珍藏版）》请在金锄头文库上搜索。
1、An Open Framework for Foundational Proof-Carrying CodeXinyu FengYale UniversityJoint work with Zhaozhong Ni (Yale, now at MSR), Zhong Shao (Yale) andYu Guo (USTC)1MotivationHow to build fully certified software systems?Source-level codeLibraries and runtime+References with weak upd.Dynamic mem. allo
2、c.Functions, exceptions, ConcurrencyI/OGarbage collectorsmalloc() (strong update)Stacks, code pointersContext switching & SchedulerDevice drivers2MotivationnAll concurrency verification assumes built-in concurrencynAssume-Guarantee (A-G) reasoningnConcurrent Separation logic (CSL)nnContext switching
3、, schedulernToo low-level to be certified in these logicsYu&Shao, ICFP04nThreads & schedulers have never been modularly certified!3MotivationnCertify all code in a single type system/program logic?nHard to combine all featuresnweak vs. strong update, functions/exceptions vs. gotos, threads vs. threa
4、d contextsnMay not be modularnVery complex, hard to usenDont know how to design such a logicnCertify modules using the most appropriate logic!nModules do not use all the features at the same timenIt is simpler to use specialized logic for each module4An Open FrameworkCertify different modules using
5、different verification systems!5ChallengesnExtensibility and opennessnnot designed for certain specific interoperationsBut can we just use MLFs, e.g. Coq?nExpressivenessntype safety, concurrency properties, partial correctness, nA general and uniform model of control flownAllow functions certified i
6、n different systems to call each othernthe key for modularity: separate verification & proof reusenPrincipled interoperation with clear meta-propertynproperties of the whole system composed of modulesNot readily supported in Coq!6Our contributionsnOCAP: an open frameworknEmbedding of different syste
7、msnTAL, non-CPS Hoare-logic, A-G reasoning, nOpen & ExtensiblenModularity with first-class code pointers Ni&Shao POPL06nSoundnessnType safety, & preservation of invariants in foreign systemsnApplicationsnTAL + memory allocation libs.nThreads + SchedulernThe first time to modularly certify both sides
8、n7OutlinenOCAP FrameworknCertifying Threads & Schedulers8OCAP RulesL Ln nOCAP : OverviewOCAPSoundnessMechanized Meta-Logic (CiC)Modeling of the machineTCBSoundL L1 1( )( )L1L1( )( )LnLnSoundMechanized Meta-Logic (CiC)Modeling of the machineC1Cn9The MachineI1f1:I2f2:I3f3:(code heap) C0r112r2r3rn(data
9、 heap) H(register file) R(state) S addu lw sw j f(instr. seq.) I(program) P:=(C,S,pc):=(H,R):=f I*pc10The OCAP Logic : OverviewnHoare-style program logic for assemblynCPS-style reasoningnAssign a precondition to each basic blocknSimilar to TAL Morrisett et al. POPL9811The OCAP Logic : OverviewI1f1:I
10、2f2:I3f3:(code heap) C0r112r2r3rn(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*pca1a2a3(spec) := f a*a12OCAP: Code pointerscodeptr(f,a) (f) = a(Spec) := f a* acodeptrNot well-founded!Support of first-class code pointers:13OCAP: Code PointersA
11、generic specification:(CdSpec) := (Assert) a Spec State Prop(Spec) := f *( ) ,S. No interoperation between multiple systems acodeptra codeptr ( ( ) )14OCAP: Foreign Languages(LangTy) L L := CiC Terms Type(CodeSpec) := CiC Terms L LInductive TalType : Type := T_int : TalType T_pair: TalType - TalType
12、- TalType Inductive Tal2Type : Type := T2_int : TalType T2_pair: TalType - TalType- TalType L L := TalType | Tal2Type | 1 := T_int | T_pair 1 1 | TalType 2 := T2_int | T2_pair 2 2 | Tal2Type15OCAP: Specifications (OCdSpec) := L L.(L L Assert)*L L(Spec) := (f1, 1), (fn, n)(Assert) a Spec State Prop(I
13、nterp) ( )L L L L Assert(LangTy) L L := CiC Terms Type(CodeSpec) := CiC Terms L LNot well-founded: ( )L La16OCAP: Specifications (OCdSpec) := (Spec) := (f1, 1), (fn, n)(Assert) a Spec State Prop(Interp) ( )L L L L Assert(LangTy) L L := CiC Terms Type(CodeSpec) := CiC Terms L L(LangID) := n nat(LangD
14、ict) D D := 1, n LangID ( L L.L L Assert) ( )L La17Selected OCAP RulesD D1 D D2; 1 2 C1 C2 : 12D D1; 1 C1: 1(link)D D2; 2 C2: 2D D ajr r ,S.a S .(codeptr(S.R(r), ) a) S (jr)a = D Dcodeptr(f, ) ,S. (f)= D D ,S. ( )L L.(D D( )=)( )L L S) = 18OutlinenOCAP FrameworknCertifying Threads & Schedulers19Thre
15、ads and SchedulernThread code C1,CnnCertified following CCAP Yu&Shao, ICFP04nAssume-Guarantee reasoningnThread modularitynDo not know about thread queueSCAPCCAP+nScheduler CSnCertified in SCAP Feng et al. PLDI06nas sequential codenManages thread queue TQnDo not touch H20Scheduler in SCAPyield: pick
16、one word (pci) from TQ si and r31 jr r31H1pc1pcnTQr31r0H1pc1pcnTQr31r0 jal yieldct: Thread code:ctct21Scheduler in SCAPyield: (ps, gs) pick one word (pci) from TQ si and r31 jr r31gsgs ( r r1,r30.r=r) Q Q, Q Q. p. Q Q r31 = Q Q r31WFTQ(Q Q)*pWFTQ(Q Q)*pH1pc1pcnTQr31r0H1pc1pcnTQr31r0ctctps Q Q.WFTQ(Q
17、 Q) * True22Embedding SCAP( (p,g) )D Dscapscap jr $ragp D DSoundness: scapscapscap C: scap ( ( scap) )D DscapscapD D Dscap, C: ( ( scap) )D DscapscapDscap scapscap 23Threads: Assume-GuaranteeSp1p2SSpec. for threads: (p, A, G)p: State Propp1p2 ?A, G: State State PropStability of p: pi S Ai S S pi SG1
18、 A2 A1, G1A2, G224CCAP embedding ccapccapccap Ci: ccapDall ccapccap , scapscap Dall; cy Ci: c y yield c ( ( ccap) ) ccapccap c ( ( ccap) ) ccapccap( (p,A,G) )ccapccap ,S. 25Certify the code ccapccapccap Ci: ccap scapscapscap Cs: scapDall ccapccap , scapscap Dall; y Cs: yDall; cy Ci: cSCAPCCAPthe “li
19、nk” ruleDall; cy Ci Cs : c y26SummarynIt is simpler and natural to certify different modules using different logicsnOCAP: framework for interoperationnEmbeddingnTAL: type systemnSCAP: non-cps logic for assemblynCCAP: Assume-guarantee reasoningnInteroperationnTAL + newpairnThreads + SchedulernTAL + GC (ongoing work by Lin, McCreight, et al.)27Future worknExplore the applicability of OCAPnInteroperation of different languagesnCurrently just for assembly languagenBut logics are at different levels (TAL, CCAP, )nMay support C + inlined assembly28Thank you!29
