A semantic model of types and machine instructions for proof-carrying code

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)=defvAbstractingoverrandm,wesaythatstda(r,m)(v)=defvIfallmemorybeyondaddress100isreadableandwritable,andtheprogramitselfoccupiesaddresses100–299,thenwemightstartwithr6=300andincreaser6astheprogramexecutes.Theprogramwillinitialize(i.e.,store)newdatastructuresbeyondr6;toensurethattheproginvariantholds,wemustcontinuallymaintaintheinvariantr6≥300.

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′toyieldthecomponentWecanabstractstdafromI106

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