Research Statement

LiminJia

Myresearchinterestsareinthefieldofprogramminglanguages.Iamparticularlyinterestedindesigningformallogics,andusingtheselogicstodevelopautomatedverificationtools,typesystems,andnewlanguagefeaturestohelpproducemorereliablesoftware.

PreviousandCurrentResearch

DuringmygraduatestudyatPrincetonUniversity,Iexploredtwomainresearchareas:oneinvolveddevelopingsystemsforverifyingmemory-safetypropertiesofsource-levelimperativeprogramminglanguages;theotherinvolveddevelopingtypesystemsthatcapturerichmemory-managementinvariantsattheassemblylanguagelevel.

VerifyingPointerPrograms

Oneofthemostimportantandenduringproblemsinprogramminglanguagesresearchistheverifi-cationofprograms,suchasthosewritteninC,thatexplicitlyallocate,deallocate,andmanipulatecomplexheap-allocateddatastructures.Improperpointeroperationsmaycauseprogramstocrashandcreateserioussecurityvulnerabilities.Unfortunately,muchofoursoftwareinusetoday,andmanynewapplicationsbeingdeveloped–especiallythoserunningonresource-scarcesystems,forinstance,embeddedsystems–areimplementedinC.Recently,greatprogresshasbeenmadeinstaticallyverifyingpointerprogramsbyusingsubstructurallogicstodescribeprogrammemory.Substructurallogicstreateachassumptionasaconsumableresourcethatcanbeusedexactlyonceinproofconstruction.Asaresult,theselogicscandescribetheshapeofheap-allocateddatastruc-turespreciselyandreasonaboutmemorystatechangeselegantly.However,existingverificationsystemsdonothavegeneralizedproofsystemstoreasonaboutexpressiveconstraintssuchasinte-gerconstraintsandsetconstraints.Asaresult,thosesystemscanonlyreasonaboutahandfulofveryspecializeddatastructuresforwhichtheyhavehard-codedtheaxioms.

Inmythesis,whichisthecombinationofaseriesofconferencepapers[2,3,4],Idesignedanewsubstructurallogicthatiscapableofgeneralconstraint-basedreasoningandexploredusingdifferentfragmentsofthelogictoverifyavarietyofpropertiesofpointerprograms.Themaingoalofmythesisistodevelopafoundationalsubstructurallogicthatiscapableofreasoningaboutmemory-safetyinvariantselegantly,and,moreimportantly,canbeusedasaunifiedunderlyinglogicforbuildingvariousverificationsystems.Thedevelopmentofthislogicpavedthewayforintegratingdifferentverificationsystemsintoone.Insuchacombinedsystem,theusershavegreatflexibilityinchoosingdifferentcombinationsoftechniquestoobtainthedesiredtrade-offbetweenthestrengthofsafetyguarantees,thecostofverification,andrun-timeoverhead.

ASubstructuralLogicwithConstraintReasoning.Togetherwithmyadvisor,Idesignedalogicforreasoningaboutmemoryinvariants(ILC)byextendingintuitionisticlinearlogicwithmechanismstoreasonaboutconstraintssuchasintegerarithmeticconstraints.WeuseILCasthebaselogicintheverificationofpointerprograms.ILC’sprooftheoryaugmentstheprooftheoryofintuitionisticlinearlogicwithanewmodalitythatconfinesformulasdescribingconstraints.Theseparationoflinearreasoningfromconstraint-basedreasoningsetsupamodularframeworkfor(1)thedesignofautomatedtheoremproversforILC,and(2)reasoningaboutILC’sdecidabilityproperties.Theabsenceofterminatingautomatedtheoremproversforlogicsthatareexpressiveenoughtoreasonaboutprogrampropertiesisoneofthebiggesthurdlestobuildingautomated

1

verificationsystems.WeidentifiedausefulanddecidablefragmentofILCandshowedhowtobuildanautomatedtheoremproverforILCbycombiningalinearlogictheoremproveranddecisionproceduresforsolvingconstraints.

DynamicHeap-shapeAssertions.Dynamicassertions,suchasthe“assert”statementinC,areanefficientmethodofensuringthatinvariantsholdatruntime.However,inordertochecktheshapeinvariantsofdatastructuresatruntime,programmershavetowritecomplexfunctionstotraversethedatastructures.Suchfunctionsoftencontainmessypointeroperationsandhencehavelittledocumentationvalue.WedesignedandimplementedanoveldynamicverificationsystemforcheckingshapeinvariantsforasubsetofCbyusinglinearlogicasthespecificationlanguageforinvariants.Thehigh-level,declarativelogicalspecificationsallowclear,compact,andsemanticallywell-defineddocumentationofheap-shapepropertiesofdatastructures.Theoperationalmeaningoftheassertionsishandledatruntimebyasimplifiedlinearlogictheoremprover.Thesedynamicallyevaluatedassertionsserveasalight-weightcomplementtostaticverificationtechniques.Selectivelyverifyingpiecesofthecodestaticallyandinsertingdynamicchecksatentrypointsfromunverifiedcodetoverifiedcodeistheidealscenariowherewegetbothstrongsafetyguaranteesonimportantpartsofthesoftwareandrelativelylowoverallcostofverification.

ALanguagewithShapePatterns.ThetypeannotationsandtypecheckingofCdoeslittletoensurememorysafety.WecouldgreatlyimprovethereliabilityofprogramsbybuildingtheshapeinvariantsandstrongtypesystemsintoimperativelanguageslikeC.Togetherwithmyadvisor,Idesignedanimperativelanguagethatallowsprogrammerstodefinerecursivedatastructuresusinglinearlogic;furthermore,programmerscanuselinearlogicalformulastoconstruct,dereference,updateanddisposeofheap-allocateddatastructures.Bycombiningnewverificationtechniqueswithamoderntypesystemforresourcecontrol,wedesignedalanguagethat,inadditiontoensuringmemorysafety,guaranteesthatshapeinvariantsholdthroughouttheexecutionoftheprogram,whichhelpstoensurecorrectness.Thedesignofthislanguagedemonstratesacombineduseofstaticanddynamiccheckstoensurememory-safetyproperties.

TypeSystemsforAssemblyCode

Typecheckingprogramsinastrongly-typedhigh-levelprogramminglanguagedoesnotnecessarilyguaranteethesafetyoftheactuallow-levelcoderunonthecomputer.Thelow-levelassemblycodeisproducedbycompilersthataretoocomplicatedtobetrusted.Onewaytoensurethesafetyoflow-levelcodeistodeveloptypesystemsforassemblylanguages.Throughcheckingthetypesafetyoftheassemblycodeitproduces,wealsogainconfidenceinthecorrectnessofthecompiler.

Typesystemsforassemblylanguagesessentiallykeeptrackofprogramstate(memory)changesastheprogramisexecuted.Recallthatsubstructurallogicscandescribememoryinvariantsele-gantly.Typesystemsforlow-levelassemblylanguagesbasedonsubstructurallogicshavetremen-dousflexibilityandexpressivenesstocaptureallsortsofmemory-safetyinvariantsthatarepresentinthetypesystemofthesourcelanguage.

Togetherwithmyadvisorandcolleagues,Idevelopedalinear-logic-basedtypesystemforassemblylanguage[1]thatiscapableofdescribingthememory-safetyinvariantsinthepresenceofmemoryallocationbothontheheapandthestack.Wealsodevelopedanalgorithmforatype-preservingtranslationfromalanguagewithstackallocation–acoreintermediarylanguagethatcapturestheessenceofstackallocationintheMicrosoftCommonLanguageInfrastructure(CLI)–toourassemblylanguage.Ourtypesystemforassemblylanguageisthefirsttobeabletohandlerealisticinvariantsforgeneralstackallocation,suchasthosepresentinCLI.

2

FutureResearch

Iplantocontinuetocombinetraditionaltypesystemswiththeoremprovingtodesignlanguagesanddeveloptoolstoprovidememory-safetyguaranteesofprograms.Inparticular,I’minterestedindevelopingtheoremproversforsoftwareverification.Automatedtheoremproversarethekeytoautomatedstaticverificationsystems.Westilldonothaveasatisfactorytheoremproverthateffectivelycombineslinearlogicreasoningandconstraintssolving:Ihadtobuildindividualtoolsforeachprototypeimplementationofourresearchprojects.Iwouldliketodevelopanextensibletheoremproverthatmodularlycombineslinearlogicreasoningandconstraintsolvingfortheoriesofconcern.Ibelievethiswillcontributesignificantlytothefieldofverifyingpointerprograms.

Iamalsointerestedincombininglinear-logic-basedstaticanddynamicverificationtechniqueswithotherformalmethods,suchasmodelchecking,todevelopacomprehensiveverificationsystemforarealimperativelanguagelikeC.Userswouldbeabletopickacombinationofverificationmethodstoachieveabalancebetweencostsandthestrengthofsafetyguaranteesaccordingtodifferentneeds.Someofthekeystepstodevelopingsuchasystemaretoprovidemodelcheckingtoolswithpreciseabstractionsoftheprogramheapextractedfromlinearlogicformulas,tocapturethememory-safetyinvariantsofprogramsthatcontainpointerarithmeticandtypecastingofpointers,andtomakethesystemscalable.

Multicoreprocessorarchitectureshavecreatedhugedemandsforlanguagedesignsthatsupportparallelization.Onewaytoextractparallelismistoruncomputationsonnon-overlappingdatastructuresindifferentthreads.Verificationtechniquesusingsubstructurallogicsanalyzedisjoint-nessofdatastructuresandtheshapesofdatastructuresoftheprogram.Applyingsubstructurallogicsinabroad,high-leveltypesystemtodescribeconditionsforparallelizablecomputationsisanewandchallengingdirectiontoutilizeformallogicstohelpsolvepracticalproblems,andIamlookingforwardtoexploringthisarea.

References

[1]L.Jia,F.Spalding,D.WalkerandN.Glew.Certifyingcompilationforalanguagewithstackallocation.

InProceedingsofthe20thIEEESymposiumonLogicinComputerScience(LICS),June2005.[2]L.JiaandD.Walker.ILC:Afoundationforautomatedreasoningaboutpointerprograms.InProgram-mingLanguagesandSystems:15thEuropeanSymposiumonProgramming,ESOP2006,LectureNotesinComputerScience3924,April2006.[3]F.Perry,L.JiaandD.Walker.ExpressingHeap-shapeContractsinLinearLogic.InProceedings

ofthe5thInternationalConferenceonGenerativeProgrammingandComponentEngineering(GPCE),October2006.[4]L.JiaandD.Walker.Linearlogic,heap-shapepatternsandimperativeprogramming.Submittedfor

publication,November2006.http://www.cs.princeton.edu/~ljia/research/papers/shapes.pdf.

3