Proof-CarryingCode
AndrewW.Appel
BellLaboratories∗andPrincetonUniversity
July16,1999
AmyP.FeltyBellLaboratories
Abstract
Proof-carryingcodeisaframeworkforprovingthesafetyofmachine-languageprogramswithamachine-checkableproof.Suchproofshavepreviouslydefinedtype-checkingrulesaspartofthelogic.Weshowauni-versaltypeframeworkforproof-carryingcodethatwillallowacodeproducertochooseaprogramminglan-guage,provethetyperulesforthatlanguageaslemmasinhigher-orderlogic,thenusethoselemmastoprovethesafetyofaparticularprogram.Weshowhowtohandletraversal,allocation,andinitializationofvaluesinawidevarietyoftypes,includingfunctions,records,unions,existentials,andcovariantrecursivetypes.
1Introduction
Whenahostcomputerrunsanuntrustedprogram,thehostmaywantsomeassurancethattheprogramdoesnoharm:doesnotaccessunauthorizedresources,readprivatedata,oroverwritevaluabledata.Proof-carryingcode[Nec97]isatechniqueforprovidingsuchassur-ances.WithPCC,thehost–calledthe“codeconsumer”–specifiesasafetypolicy,whichtellsunderwhatcondi-tionsawordofmemorymaybereadorwrittenorhowmuchofaresource(suchasCPUcycles)maybeused.Theprovideroftheprogram–the“codeproducer”–mustalsoprovideaprogram-verification-styleproofthattheprogramsatisfiestheseconditions.Thehostcom-putermechanicallycheckstheproofbeforerunningtheprogram.
TwosignificantadvantagesofPCCarethat(1)theseproofscanbeperformedonthenativemachinecode,so
upd(f,d,x,f′)=def∀z.d=z∧f′(z)=x∨d=z∧f′(z)=f(z)
add(d,s1,s2)(r,m,r′,m′)=defupd(r,d,r(s1)+r(s2),r′)∧m=m′.addi(d,s,c)(r,m,r′,m′)=defupd(r,d,r(s)+c,r′)∧m=m′
load(d,s,c)(r,m,r′,m′)=defreadable(r(s)+c)∧upd(r,d,m(r(s)+c),r′)∧m=m′
store(s1,s2,c)(r,m,r′,m′)=defwritable(r(s2)+c)∧upd(m,r(s2)+c,r(s1),m′)∧r=r′jump(d,s,c)(r,m,r′,m′)=def∃r′′.upd(r,17,r(s)+c,r′′)∧upd(r′′,d,r(17),r′)∧m=m′
bgt(s1,s2,c)(r,m,r′,m′)=defr(s1)>r(s2)∧upd(r,17,r(17)+c,r′)∧m=m′∨r(s1)≤r(s2)∧r=r′∧m=m′beq(s1,s2,c)(r,m,r′,m′)=defr(s1)=r(s2)∧upd(r,17,r(17)+c,r′)∧m=m′∨r(s1)=r(s2)∧r=r′∧m=m′
Figure1:Semanticdefinitionofmachineinstructions.
2Example
Toillustrate,weuseanimaginaryword-addressedma-chinewithasimpleinstructionsetandinstructionen-coding.
OPCODE
Werefertotheaxiomsasthesafetypolicy.ForEx-ample1,wewillusethefollowingsafetypolicy:1.2.3.4.5.6.7.
∀v.(v≥50)→readable(v)∀v.(v≥100)→writable(v)
∀r,m.(r(17)=r0(7))→safe(r,m)r0(1)>50r0(17)=100m0(100)=2210m0(101)=4077
addaddiloadstorejumpbgtbeq
rd←rs1+rs2rd←rs+crd←m(rs+c)m(rs2+c)←rs1
rd←pc;pc←rs+c
ifrs1>rs2thenpc←pc+cifrs1=rs2thenpc←pc+c
Example1.Wewishtoverifythesafetyofthefol-lowingshortprogram.Thecodeproducerwillprovidetheprogram(i.e.,inthiscasethesequenceofintegers(2210,4070))andaproofthatiftheseintegersareloadedataddress100thenitwillbesafetojumpthere.Thepro-gram’spreconditionisthatregister1pointstoarecordoftwointegersandregister7pointstoareturnaddress.100:2210r2←m(r1)
101:4070jump(r7);r0←pc
Thelogiccomprisesasetofinferencerulesandasetofaxioms.Theinferencerulesarestandardnatural-deductionrulesofhigher-orderlogicwithnaturalnum-berarithmeticandinduction,augmentedwithjustafewpredicatesandrulesconcerningthereadability,writabil-ity,and“jumpability”ofmachineaddresses,andthede-codingandsemanticsofmachineinstructions.
2
Axioms1and2describewhataddressesarereadableandwritable.Axioms3–7describetheinitialstateofthemachine,comprisingaregister-bankr0andamemorym0,eachofwhichisafunctionfromintegerstointegers.Axiom3saysthatanyfuturestater,mwhoseprogramcounterr(17)isequaltowhat’sinr0(7)isasafestate;orincommonterms,initiallyr7isavalidreturnaddress(wewriter(7)andr7interchangeably).Axiom4says
0isanaddressinthereadablerange,andaxiom5thatr1
saysthattheprogramcounterr17isinitially100.Theremainingaxiomsdescribetheuntrustedcodethathasjustbeenloaded.
WehaveimplementedourlogicinTwelf[PS99],whichisanimplementationoftheEdinburghlogicalframework[Pfe91].AllthetheoremsinthispaperhavebeencheckedinTwelf.
Theorem.safe(r0,m0).
Thistheoremistheonethatthecodeproducermustprove;thecodeconsumerwillchecktheproofbeforejumpingtoaddress100.Butbeforedescribingtheproof,wemustshowtheinferencerulesforreasoningaboutmachineinstructions.
format(w,a,b,c,d)=def0≤a<16∧0≤b<16∧0≤c<16∧0≤d<16∧w=a∗163+b∗162+c∗16+d.decode(v,m,i)=def
(∃d,s1,s2.format(m(v),0,d,s1,s2)∧i=add(d,s1,s2))∨(∃d,s1,c.format(m(v),1,d,s1,c)∧i=addi(d,s1,c))∨...
Figure2:Instructiondecoding.
3Instructionexecution
Eachinstructiondefinesarelationbetweenthemachinestate(registers,memory)beforeexecutionandthema-chinestateafterwards.Wetreattheprogramcounteraspartoftheregisterset(r17)eventhoughit’snotreallynamableinaninstructionopcode.Figure1showsthedefinitionofthisrelationforeachoftheinstructionsadd,addi,load,andsoon.
OnavonNeumannmachine,eachinstructionisrep-resentedinmemorybyaninteger.Ourdecoderelation(Figure2)isapredicateonthreearguments(v,m,i)andsaysthataddressvinmemorymcontainstheencodingofinstructioni.
Wecannowwriterelationstep(r,m,r′,m′)(Figure3)whichsaysthattheexecutionofoneinstructioninstate(r,m)leadstostate(r′,m′).Thisholdsonlyforsafeandlegalinstructionexecutions,becausethedefinitionoftheloadrelationrequiresthattheloadedaddressberead-able,andthedefinitionofstorerequiresthatthestoredaddressbewritable,andthedecoderelationfailstoholdatallforillegalinstructions.
Finally,wecapturethenotionofcontinuedexecu-tionbytheinferencerulemultistep(Figure3),whichisacoinductionprinciplebased(loosely)ontheFloyd-Hoarewhilerule.
Ourdefinitionsallowforthepossibilitythatastoreinstructionwilloverwritetheprogram,whichallowsustoprovethesafetyofself-modifyingcode.Butoursim-pleexampledoesnotoverwriteitself,andthisfactisanecessarypartofourinvariant:prog(m)=def
decode(100,m,load(2,1,0))∧decode(101,m,jump(0,7,0))
Nowourglobalinvariantisjustthecombinationoftheproginvariantwithallthelocalones:Inv(r,m)=defprog(m)∧(r(17)=100∧I100(r,m)∨r(17)=101∧I101(r,m)∨jumpable(r(17)))
Toproveourtheoremsafe(r0,m0)weusethemul-tisteprule.FirstweshowInv(r0,m0),thenthatInvispreservedunderthesteprelation.
Axioms6and7,alongwiththedefinitionofthedecoderelation,provethatprog(m0)holds.Axiom5(r0(17)=100)meansthattheremainingproofobliga-tionforInv(r0,m0)isI100(r0,m0),whichcanbeproveddirectlyfromaxioms3,4,and1.
Toshowthattheinvariantisconserved,weworkbycases:
•r17=100∧I100(r1,m1).Byprog(m1)wehave
1,m1,load(2,1,0)).decode(r17Lettingr2=r1[17→
1+1,2→m1(r1)]andm2=m1,andusingr171
1)fromI1122readable(r1100,wehavestep(r,m,r,m).
221=r2,byISincer7100wehavejumpable(r7).Thusr17=7
101∧I101(r2,m2)isproved.Sincem1=m2,prog(m2)holds.
1111=101∧I•r17101(r,m).Byprog(m)wehave
1,m1,jump(0,7,0)).Lettingr2=r1[17→decode(r17
1,0→r1],wehavejump(0,7,0)(r1[17→r1+r71717
1211],m,r,m)bythedefinitionofjump.Thuswehavestep(r1,m1,r2,m1).Wecanusethedefinition
1),toshowoftheupdrelation,alongwithjumpable(r73
4Theglobalinvariant
Toproveourprogramsafe,weconstructaninvariantInv
thatholdsatalltimes.Westartbyinformallyannotatingeachinstructionwithaprecondition.
I100(r,m)=jumpable(r7)∧readable(r1)100:2210r2←m(r1)
I101(r,m)=jumpable(r7)101:4077jump(r7)where
jumpable(v)=def∀r′,m′.r′(17)=v→safe(r′,m′)).
step(r,m,r′,m′)=def∃i,r′′.decode(r(17),m,i)∧upd(r,17,r(17)+1,r′′)∧i(r′′,m,r′,m′)Inv(r,m)
∀r1,m1.Inv(r1,m1)→(safe(r1,m1)∨(∃r2,m2.step(r1,m1,r2,m2)∧Inv(r2,m2)))
readable(v)∧readable(v+1)record2
∧m(v):mτ1∧m(v+1):mτ2
readable(v)∧readable(v+1)list
∧m(v):mτ∧m(v+1):mlist(τ)
eruleshownabovecanbeprovedasa
theorem,directlyfromthedefinitionofrecord2.
Wecangoontodefineuniontypes,listtypes,andsoon,withcorrespondingtraversaltheorems.ButNecula’sPCCsystemgivesnorulesforcreation(i.e.,allocationandinitialization)ofdatastructuressuchasrecordsandlists.Fromourdefinitionofrecord2wecouldcertainlyprovethetheorem,
readable(v)∧readable(v+1)m(v):mτ1∧m(v+1):mτ2
i
4
Butthisisnotenough!Anyprogramthatcreatesanewrecordvaluemustinitializeitbystoringtwovaluesintomemory.Thestepruleforthestoreinstructionisstore(s1,s2,c)(r,m,r′,m′)=defwritable(r(s2)+c)∧
upd(m,r(s2)+c,r(s1),m′)∧r=r′
whichrelatesamemorym(beforethestore)toamem-orym′(afterthestore).Nowsupposewehavethefol-lowingprogramfragment:
I103(r,m)=r1:mint×(int×int)∧r3:mint103:m(r2)←r3
I104(r,m)=r1:mint×(int×int)
∧r3:mint∧m(r2)=r3
104:m(r2+1)←r3
I105(r,m)=r1:mint×(int×int)∧r2:mint×intAfterstoringtwointegersintomemoryataddressesr2andr2+1wecanlegitimatelyusetherecord2
mightuseadatastructuretokeeptrackofwhichblocksofmemoryareallocated.
Thetypingjudgementv:mτ1×τ2shouldimplythattheaddressesvandv+1areintheallocatedset.Wecanmakethisexplicitbymakingtheallocatedsetaaparameterofthetypingjudgement:v:a,mτ.Nowwedefinerecordtypesabitdifferentlythanintheprevioussection(whereaisanallocationpredicateandv∈aissyntacticsugarfora(v)):
record2(τ1,τ2)(a,m)v=defv∈a∧(v+1)∈a
∧readable(v)∧readable(v+1)
∧τ1(a,m)(mv)∧τ2(a,m)(m(v+1))
Maintainingtheallocationpointer.Considerapro-gramthatusesregisterr6asanallocationpointer,sothatthe“standard”allocatedpredicateisa(v)=defv Allocatingarecord.Figure4showsaprogramthatcreatesanewrecordvaluebystoringthetwofieldsatlocationsr6andr6+1andthenincreasingr6by2.Clearly,atthepointI109r2satisfiesalltheconditionsintheright-handsideofthedefinitionofrecord2(τ,τ)(stda(r,m),m),provingthejudgementr2:stda(r,m),mτ×τ. Butatthesametime,thereisapre-existingrecordvalueinr1thatwillstillbeneededtouseafterthenewvalue–thatis,boththepreconditionI106andthepost-conditionI110mentionr1:a,mτ.Thetrickistomaintainthisjudgementevenasthestorescreate“different”m’sandincreasingr6creates“different”asets.5 v:m′τ1×τ2 buthowcanweorganizetheproofsoastoestablishthatx=v? Thesolutionistoreasoncarefullyaboutheapalloca-tion,distinguishingtheallocatedregionoftheheapfromtheunallocatedregion,asthenextsectionwillexplain. 6HeapAllocation Acall-by-valuepurefunctionalprogramallocatesnewdata-structurevaluesonaheap,andneverupdatesoldvalues.(Imperativelanguagesaremuchhardertoreasonabout,soweleavethatforfuturework.)Theprogram(andrun-timeenvironment)keepstrackofwhichloca-tionsareallocatedandwhicharefreeontheheap.Inaverysimplesystemanallocationpointer–aregisterormemorylocation–pointstotheboundarybetweenallo-catedandunallocatedmemory.Amorecomplexsystem 106:107:108:109: I106(r,m)=r6≥300∧r1:stda(r,m),mτm(r6)←r1 I107(r,m)=r6≥300∧r1:stda(r,m),mτ∧m(r6):stda(r,m),mτm(r6+1)←r1 I108(r,m)=r6≥300∧r1:stda(r,m),mτ∧m(r6):stda(r,m),mτ∧m(r6+1):stda(r,m),mτr2←r6+0 I109(r,m)=r6≥300∧r1:stda(r,m),mτ∧m(r2):stda(r,m),mτ∧m(r2+1):stda(r,m),mτ∧r2=r6r6←r6+2 I110(r,m)=r6≥300∧r1:stda(r,m),mτ∧r2:stda(r,m),mτ×τ Figure4:Aprogramthatallocatesandinitializesarecord. Wewilldefineavalidtypeasonesatisfyingtheseconditions: valid(τ)=def ∀a,a′,m,v.(a⊂a′)→τ(a,m)v→τ(a′,m)v∧∀a,m,m′,v.(∀x∈a.m(x)=m′(x))→ τ(a,m)v→τ(a,m′)vThefirstconditionisthatatypingjudgementv:a,mτisinvariantunderincreasingthesizeoftheallocatedset;thesecondisthatthejudgementisinvariantunderstor-inganyvalueatanyunallocatedlocation. Ifτisavalidtype,thenthejudgementr1:a,mτwillbepreservedthroughalltheoperationsbetweenI106andI110.Eachtypingpredicatethatwewishtouseinourproofofsafetymustbeprovedvalid.Wewillshowsuchtheoremsinthenextsection. Morrisettetal.[MWCG98]showhowtoprovesafetyofallocationbasedonatypesystemforpartiallyinitial-izedrecords.Wehavenotchosentodothis;instead,theapproachwehaveshowninthissectionusesdataflowanalysistoreasonaboutthecontentsofthepartiallyini-tializedrecord.Webelievethiswillworkwell,sincerecordinitializationisanessentiallylocalphenomenon. consttyi(a,m)v=defv=i Theconstanttype,thatis,6:a,mconstty(6).char(a,m)v=def0≤v<256 Thecharacter(ortinyinteger)type.boxed(a,m)v=defv≥256 Thetypeofboxed(noncharacter)values.refτ(a,m)v=defv∈a∧readable(v)∧τ(a,m)(mv) Thetypeof(immutable)referencestomemorywordscontainingvaluesoftypeτ.arefτ(a,m)v=defv∈a∧readable(v)∧ ∃a′.a′⊂a∧v∈a′∧τ(a′,m)(mv) Thetypeofacyclicreferences,thatis,therefer-enceddatastructuredoesnotcontainpointersbacktoaddressv.offsetiτ(a,m)v=defτ(a,m)(v+i) Thetypeofvaluesvsuchthatv+ihastypeτ.fieldiτ=defoffseti(refτ) Thetypeofarecordfieldatoffseticontainingavalueoftypeτ.Ifacyclicrecordsaredesired,thenarefcanbeusedinsteadofref.union(τ1,τ2)(a,m)v=defτ1(a,m)v∨τ2(a,m)v Thetypeτ1∪τ2ofvaluesthatbelongeithertoτ1orτ2.intersection(τ1,τ2)(a,m)v=defτ1(a,m)v∧τ2(a,m)v Thetypeτ1∩τ2.record2(τ1,τ2)=deffield0τ1∩field1τ2 Adefinitionofthetwo-elementrecordtypeequiva-lenttotheonegiveninsection6butmoreconcise.6 7Typeconstructors AlmostallthetypesusedinMLprogramscanbedefinedandprovedvalidinoursystem:recordtypes,taggeduniondatatypes,functiontypes,abstracttypes,polymor-phictypes,andcovariantrecursivetypes.Wehavenotyetsucceededindefiningcontravariantrecursivetypes,asthenextsectionwilldiscuss.Westartwithsomeprimitives: sum(τ1,τ2)=def record2(constty0,τ1)∪record2(constty1,τ2)Ataggeddisjointsumtype.money=defrecord2(constty0,int) ∪record2(constty1,int)∪record3(constty2,int,int)EquivalenttotheMLdatatype, money=COINofint |BILLofint |CHECKofint*int existential(F)(a,m)v=def∃τ.(Fτ)(a,m)v∧valid(τ) Anexistentialtype,usefulindefiningabstractdatatypes[MP88]andfunctionclosures[MMH96].universal(F)(a,m)v=def∀τ.valid(τ)→(Fτ)(a,m)v Anuniversaltype,usefulforpolymorphicfunc-tions.Nowwemustproveallthesetypesandconstructorsvalid.Thetypesconstty,char,boxedareinvariantwithrespecttoincreasingaorupdatingmatanunallocatedlocationbecausetheirdefinitionsdon’tusetheaormargumentatall. Typeref(τ)isvalidifτisvalid: 1.a⊂a′→τ(a,m)w→τ(a′,m)wforallw,sotheimplicationwillholdfortheparticularw=m(v).2.ifm=m′atallallocatedlocations,thenτ(a,m)(m(v))→τ(a,m′)(m(v))byvalidityofτ.Andsincev∈a,thenm(v)=m′(v),soτ(a,m′)(m(v))→τ(a,m′)(m′(v))bycongruence.Offsetiτisvalidifτisvalidbyinstantiationofv+iforvinthedefinitionofvalidityofτ. Unionandintersectiontypesarevalid(iftheircom-ponentsarevalid)byanequallysimpleargument. Avalidtypeconstructorisonethatpreservesvalidity,asdorefandoffset(i).Itiseasytoshowthatthecompo-sitionofvalidconstructorspreservesvalidity;therefore,fieldtypes,recordtypes,andsumtypesarevalidiftheircomponenttypesarevalid. Itistrivialtoprovethatthetypeexistential(F)isvalidifFisavalidconstructor. machine-codeaddresseswitharguments–belongtothecodeptrtype.Acontinuationclosure(cont)isacodepointerwithanenvironment.Andafunctionclosure(func)isalsoacodepointerwithanenvironment,buttheargumentsofthiscodepointerincludeacont.AcompilercouldgeneratetheseclosuresbyfollowingthetypedclosureconversionalgorithmofMorrisettetal.[MWCG98]. Acodeptrisanaddresstowhichcontrolmaybepassedprovidedthatitspreconditionismet.Inatype-basedproof,thepreconditionismainlyintheformoftypingjudgements.Wecantakeaddress106fromFig-ure4asanexample;wecanjumptolocation106fromanymachinestatesatisfyingI106andtheproginvariant.Letusseparatethisinvariantintotwoparts,the“stan-dard”invariantandthepartspecifictoentry-point106:stdp(r,m)′I106(r,m) =prog(r,m)∧r6≥300 =r1:stda(r,m),mτ Noticethatentry-point106usesthe“standard”repre-sentationoftheallocatedset,thatis,stda(r,m).Notallprogramlocationsdo;aprogramisfreetospillr6toamemorylocation,ortodeferincrementingr6untilase-riesofallocationsiscomplete.Insuchcases,aprogrampoint’sallocated-setwouldberepresentedasv oftheinvariantthatdealsjustwiththeformal-parametertype(s)ofthatentrypoint:P106(a,m)r=r1:a,mτ Thispredicatehasalmosttheformofatype,exceptwithanrparameterinsteadofv.Thatis,itspecifiesthe“type”oftheregisterbank,orrather,thetypesofsomesubsetoftheregisters–theformalparametertypes.Foranysuchparameter-preconditionP,wedefinecodeptr(P)(a,m)v=def ∀r′,m′.r′(17)=v ∧stdp(r′,m′) ∧P(stda(r′,m′),m′)(r′)→safe(r′,m′) ThissaysthatvisacodeptrwithformalparametersPif,foranyfutureregister-bankr′andmemorym′,7 8Functiontypes Wewillbuildfunctionvalues(andfunctiontypes)inthreestages.First-ordercontinuations–thatis, iftheprogram-counterisatlocationv,thestandard-preconditionstdpholds,andthetypesoftheregisterssatisfyP,thenit’ssafetocontinue. Inorderforcodeptr(P)tobeavalidtype,Pmustbeavalidregister-type–thatis,itmustbeinvariantwithre-specttoincreasingtheallocatedsetormodifyingmem-oryatunallocatedlocations.ItiseasytoshowthatP106isvalidifτisvalid.Ingeneralifτ1,τ2,...arevalidtypes,thenthepredicateri1:a,mτ1∧...rik:a,mτk isavalidformal-parameterspredicate. Letusdefineafamilyofpredicatesparamsk–forvar-iousk–asthestandardcallingsequenceofkarguments:params1(τ1)(a,m)r=def r1:a,mτ1params2(τ1,τ2)(a,m)r=def r1:a,mτ1∧r2:a,mτ2params3(τ1,τ2,τ3)(a,m)r=def r1:a,mτ1∧r2:a,mτ2∧r3:a,mτ3 Thus,withrespecttotheprogramofFigure4wecanmakethefollowingjudgement: stdp(r,m)→106:stda(r,m),mcodeptr(params1(τ)).Continuationclosures.Inaprogramminglanguagewithnestedlexicalscopesforfunctiondefinitions,aninnerfunctionmayhavefreevariables(whichareboundonlyinanouterscope).Theimplementationofsuchafunctionmustincludebothcontrol(e.g.,acodepointer)andenvironment(adatastructureinwhichvaluesforthefreevariablescanbefound).Sincetwofunctionsofthesametypemayhavedifferentsetsoffreevariables,thetypeoftheenvironmentshouldnotbepartofthefunc-tiontype.Wesolvethisprobleminthestandardway:weuseanexistentialtypetohidethetypeoftheenvi-ronment[MMH96]. Acontinuationisafunctionthatneverreturns(orrather,itsreturnisthecompletionofthewholepro-gram).Continuations,likefunctions,needclosuresandenvironments.Foranytypeτ,cont(τ)isthecontinuationtakingaτargumentinregister1.However,thecodeen-trypointwillalsohavetotakeanenvironment(oftypeσ)inregister2. cont(τ)=def existential(λσ.record2(codeptr(params2(τ,σ)),σ)) 8 Toapplyacontinuationvaluev,onemustfirstfetchthecodeptrcfromm(v+0)andputitinsomeregister,sayr5.Onemustputavalueoftypeτinr1.Onemustfetchtheenvironmentefromm(v+1)intor2.Onemustensurethatthestandardpreconditionstdp(r,m)holds.Theorem:Thenitissafetojumptotheaddresscon-tainedinr5.Proof:byexpansionofdefinitions.Functionclosures.Afunctionisjustacontinuationwithanadditionalargumentthatisitselfacontinuation.Thatis,thefunctiontypeα→βtakesoneargumentthatisavalueoftypeα,andanotherargumentoftypecont(β).Sincefunctionsmayhavefreevariables,wemakefunctionclosuresinthesamewayasforcontin-uations–sothecodeptrcomponentofafunctionhasanotherargumentoftypeσ,theenvironmenttype.func(α,β)=defexistential(λσ. record2(codeptr(params3(α,cont(β),σ)),σ))Callingafunctionisdonealmostexactlyascallingacontinuation,exceptthatr1containstheargument,r2containsthecontinuation-closure,andr3containsthefunctionenvironment. Thetype-constructorscontandfuncarevalidbecausetheyarejustcompositionsofothervalidconstructors(existential,record,codeptr,params). Wehavedescribedfunctionswithheap-allocatedcon-tinuations–notstack-allocatedframes–becausetheyareeasiertoreasonabout,easiertoimplement,suit-ablyefficient,andusedbyacompiler[Sha98]thatcanplausiblyserveasafront-endforourPCCsystem.Ofcourseitisalsopossibletoreasoneffectivelyaboutstack-allocatedframes[MCGW98,KKR+86]. 9RecursiveDatatypes Inordertodefinerecursivedatatypes,weintroduceasubtypingrelationdefinedaslogicalimplication:subtype(τ1,τ2)=def∀a,m,v.τ1(a,m)(v)→τ2(a,m)(v).Wewriteτ1⊑τ2todenotethisrelation.Usingthisrela-tion,wedefinethefollowingrecpredicate: rec(f)=def∀τ.valid(τ)→f(τ)⊑τ→τ(a,m)(v)Therecursivetypesarealltypesrec(f)forwhichtheleastfixedpointoftheargumentfunctionfisrec(f).It canbeshownthatanyfunctionfthatpreservesvalidityandalsosatisfiesthefollowingmonotonepredicatehasthisproperty. monotone(f)=def∀τ1,τ2.τ1⊑τ2→f(τ1)⊑f(τ2)Inparticular,weprovethatwheneverfsatisfiestheseproperties,bothf(rec(f))⊑rec(f)andrec(f)⊑f(rec(f))hold,andthusthefollowingtheoremholds. preserves roll rec(f)(a,m)(v)↔f(rec(f))(a,m)(v) mono(f)validwherevalid valid union mono(f)=defpreserves tm:tp->type.form:tp. pf:tmform->type. lam:(tmT->tmU)->tm(TarrowU).@:tm(TarrowU)->tmT->tmU.%infixleft20@. and:tmform->tmform->tmform.%infixright12and. forall:(tmT->tmform)->tmform.and_i:pfA->pfB->pf(AandB).and_e1:pf(AandB)->pfA.and_e2:pf(AandB)->pfB.forall_i:({X:tmT}pf(AX))->pf(forallA).forall_e:pf(forallA)->{X:tmT}pf(AX). ref:tm(tyarrowty)= lam3[T][S][V]fstS@Vand readable@VandT@S@(sndS@V).offset:tm(intarrowtyarrowty)=lam4[I][T][S][V](T@S@(V+I)).field:tm(intarrowtyarrowty)=lam2[I][T](offset@I@(ref@T)).record2:tm(tyarrowtyarrowty)=lam2[T][U](intersect@ (field@0@T)@(field@1@U)).listf:tmty->tm(tyarrowty)=[T](lam[T’](union@ (constty@(const0))@(intersect@boxed @(record2@T@T’)))). list:tm(tyarrowty)=(lam[T](rec@(listfT))). Ametalogic(Twelf)typeisatype,anobject-logictypeisatp,andaprogramming-languagetypeisaty(whichisnotinthecorelogicsinceitisadefinitionatthediscretionofthecodeproducer).Object-logictypesareconstructedfromint,thetypeformofformulasoftheobjectlogic,andthearrowconstructor.Object-leveltermsoftypeThavetype(tmT)inthemeta-logic.Quantifyingatthemetalevelallowsustoencodepolymorphicobject-leveltypes.Termsoftype(pfA)aretermsrepresentingproofsofobjectformulaA.Thedeclarationsbeginningwithlamintroducecon-stantsforconstructingtermsandformulas.Notethattheuniversalquantifierforallispolymorphic;uppercaselettersdenotevariables,andfreevariablesareimplicitlyquantifiedattheoutermostlevel.Bracesareusedforexplicitquantification.Thelastfivedeclarationsencodetheintroductionandeliminationrulesofnaturaldeduc-tionforconjunctionanduniversalquantification.Thecompleteencoding(about100linesofTwelf)includestheremaininginferencerulesofhigher-orderlogic,anencodingofintegers(includingarithmeticoperatorsandnaturalnumberinduction),themultisteprule,andtheaxiomsofthesafetypolicy.Allotherobjectsaredefini-tionsandtheoremsbuiltfromthiscoresignature.ThefollowingaretheTwelfdefinitionsofsomeofthetypeconstructorsaswellasthepolymorphiclistspresentedinsection9. ty:tp=statearrowintarrowform. Thetydeclarationgivesthetypeforpredicatesrepre-sentingMLtypes.Somedefinitionsareomitted.Forex-amplelam4isdefinedintermsoflamandbinds4vari-ables,andstateis(pairallocsetmemory)wherepairispolymorphic,definedintheusualwaywithλ-calculus.Thefollowingtheoremjustifiestheuseofrecinthedefinitionoflist. vm_listf:pf(validtype@T)->pf(valid_mono@(listfT))=[P:pf(validtype@T)](vm_unionvm_constty(vm_intersectvm_boxed(vm_record2 (vm_validtypeP)vm_id))). Thistheoremillustratestheapplicationofonelemmapertypeconstructor.Thesearethelemmasstatingthattheconstructorpreservesvalidityandmonotonicity.Thevm_uniontheorem,forinstance,waspresentedintheprevioussection. 11ConclusionandFutureWork Wehavedescribedaframeworkforproof-carryingcodewhichshouldbesufficientlygeneraltoaccommodaterealprogramminglanguagesonrealmachines.Machineinstructionsets.Tohandlerealmachines,weplantoencodeinstructionsetarchitecturessuchastheSparcandPentium;wewillhavetohandlevariablesizeinstructionsandbyteaddressing.10 Contravariantrecursivetypes.Manyrealprogram-minglanguages—ML,Java,C—havecontravariantre-cursivetypessuchasthisone: datatypeexp=APPofexp*exp |LAMofexp->exp Ourcurrenttypeframeworkcannothandlethistypebe-causeoftheoccurrenceofexptotheleftofthearrowintheLAMconstructor.WeplantoadaptthemodeloftypesinMacQueenetal.[MPS86]orinMitchellandViswanathan[MV96]toournotionoftypesaspredi-catesonmachinestates.Doingsorequirestheformal-izationoftheBanachfixedpointtheoremoncompletemetricspaces. Mutablefields.Wealsoplantodescribemutabledatastructures,suchasMLrefsandJavaobjects.Handlingreferenceswillinvolveallowingformutablememorylo-cations,whichwillrequireamorecomplexnotionofal-location,andthusamorecomplexvalidtypepredicate.Fω.Ourlonger-rangeplanistocovermoreoftypesusedbyaproductioncompilerforalanguagesuchasML.Inparticular,weplantoincorporatethetypesystemoftheFLINTintermediatelanguage[Sha98](whichwillalsocompileJava[LST99]),forwhichwewillhavetoencodethetypesandkindsoftheFωpolymorphicλ-calculus[Gir72,Rey74]. Othertypesystems.Toshowthatourapproachtosafetypolicies(whichmovesinformationfromthetrustedcomputingbaseintoasemanticmodelbuiltfromfirstprinciples)istrulyuniversal,weplantobuildamodelofatypesystemthatispossiblyquitedifferentfromthatofML.OnepossibilityisthetypesystemofTouchstone[Nec98]whichhasmutablerecords,butnorecursivetypesoruniontypes;orthetypedassemblylanguageofMorrisettetal.[MWCG98]. Concurrency.Ourmodelissequential.Concurrencyandasynchronousexceptionscanbehandledbyassum-ing(inthesteprelation)thatsomeportionsofmemorycanchangebetweensuccessivemachineinstructions,andsomeportionswillnot.Thesafetypolicymustguar-anteethatcertainmemorylocations(i.e.unsharedvari-ablesofthisthread)arepreservedunchanged. 11 Automatingproof.Inanearlierversionofoursys-tem,webuiltaprototypetheoremproverwhichauto-maticallyprovedsafetyofsimpleprogramsthattraverseandallocatelists.Wehavelotsofideasabouthowtoaugmentthisprover.Indoingso,itwillbenecessarytokeepproofssmall.Ourgoalistodevelopasetoflem-masthatallowustobuildproofsfullyautomaticallythatarelinearinthesizeofthetype-annotatedintermediaterepresentationofthecompiledprogram;webelievethisispossibleforthekindsofsafetyproofsweareconsid-ering.Anexampleillustratingthisideaisthevm_listtheoremintheprevioussectionwhoseproofusesex-actlyasmanylemmaconstructorsasthedescriptionofthelistftypeusestypeconstructors. Acknowledgements.WethankNeophytosMichaelforassistanceinimplementingthetoy-machinede-codefunctioninTwelf;RobertHarper,FrankPfenning,CarstenSch¨urmannforadviceaboutencodinglogicsinTwelf;DougHowe,DavidMacQueen,andJonRieckeforadviceaboutrecursivetypes;GregMorrisettforcommentsonanearlydraftofthepaper. References J.-Y.Girard.Interpr´etationFonctionnelleetEliminationdesCoupuresdansl’Arithm´etiqued’OrdreSup´erieur.PhDthesis,UniversityofParisVII,1972. [KKR+86]D.Kranz,R.Kelsey,J.Rees,P.Hudak, J.Philbin,andN.Adams.ORBIT:Anopti-mizingcompilerforScheme.SIGPLANNotices(Proc.Sigplan’86Symp.onCompilerConstruc-tion),21(7):219–33,July1986. [LST99]ChristopherLeague,ZhongShao,andValery Trifonov.Representingjavaclassesinatypedintermediatelanguage.InProc.1999ACMSIG-PLANInternationalConferenceonFunctionalProgramming(ICFP’99),page(toappear),NewYork,1999.ACMPress. [MCGW98]GregMorrisett,KarlCrary,NealGlew,and DavidWalker.Stack-basedtypedassemblylan-guage.InACMWorkshoponTypesinCompila-tion,Kyoto,Japan,March1998. [MMH96]YasuhikoMinamide,GregMorrisett,andRobert Harper.Typedclosureconversion.InPOPL’96:The23rdACMSIGPLAN-SIGACTSympo-siumonPrinciplesofProgrammingLanguages,pages271–283.ACMPress,January1996.[Gir72] [MP88] [MPS86] JohnC.MitchellandGordonD.Plotkin.Ab-stracttypeshaveexistentialtype.ACMTrans.onProgrammingLanguagesandSystems,10(3):470–502,July1988. DavidMacQueen,GordonPlotkin,andRaviSethi.Anidealmodelforrecursivepoly-mophictypes.InformationandComputation,71(1/2):95–130,1986. [MV96] J.C.MitchellandR.Viswanathan.Effec-tivemodelsofpolymorphism,subtypingandrecursion.In23rdInternationalColloquiumonAutomata,Languages,andProgramming.Springer-Verlag,1996. [MWCG98]GregMorrisett,DavidWalker,KarlCrary,and NealGlew.FromSystemFtotypedassem-blylanguage.InPOPL’98:25thAnnualACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,pages85–97.ACMPress,January1998. [Nec97]GeorgeNecula.Proof-carryingcode.In24th ACMSIGPLAN-SIGACTSymposiumonPrin-ciplesofProgrammingLanguages,pages106–119,NewYork,January1997.ACMPress.[Nec98] GeorgeCiprianNecula.CompilingwithProofs.PhDthesis,SchoolofComputerSci-ence,CarnegieMellonUniversity,Pittsburgh,PA,September1998. FrankPfenning.LogicprogrammingintheLFlogicalframework.InG´erardHuetandGor-donPlotkin,editors,LogicalFrameworks,pages149–181.CambridgeUniversityPress,1991.FrankPfenningandCarstenSch¨urmann.Systemdescription:Twelf—ameta-logicalframeworkfordeductivesystems.InThe16thInternationalConferenceonAutomatedDeduction.Springer-Verlag,July1999. JohnC.Reynolds.Towardsatheoryoftypestructure.InProc.ParisSymp.onProgramming,volume19ofLectureNotesinComputerSci-ence,pages408–425,Berlin,1974.Springer.ZhongShao.Typedcross-modulecompila-tion.InProc.1998ACMSIGPLANInterna-tionalConferenceonFunctionalProgramming(ICFP’98),pages141–152,NewYork,1998.ACMPress. [Pfe91] [PS99] [Rey74] [Sha98] [WLAG93]R.Wahbe,S.Lucco,T.Anderson,andS.Gra-ham.Efficientsoftware-basedfaultisolation.InProc.14thACMSymposiumonOperatingSys-temPrinciples,pages203–216,NewYork,1993.ACMPress. 12 因篇幅问题不能全部显示,请点此查看更多更全内容
Copyright © 2019- jqkq.cn 版权所有 赣ICP备2024042794号-4
违法及侵权请联系:TEL:199 1889 7713 E-MAIL:2724546146@qq.com
本站由北京市万商天勤律师事务所王兴未律师提供法律服务