王俊吉-RustConf2023-RustBelt.pptx

1、第三届中国第三届中国Rust开发者大会开发者大会王俊吉RustBelt-Rust的形式化语义模型的形式化语义模型OutlineBackground RustBelt Project Rust Types OverviewRust SemanticsType SystemThe own PredictExclusive Ownership&Mutable BorrowExamplesRcLogics Hoare Logic Separation LogicBackgroundERC Project RustBelt2015-2021Unlike C/C+,Rust is a safe langu

2、ageBut,like C/C+,Rust is also an unsafe languageThere are guaranteed memory safety,thread safety,.There are plenty of unsafe codes in Rusts standard library.use after freedata racearray-index overflowuse after freedata racearray-index overflow?.RustBelt ProjectBackgroundRalf Jung,et.al.RustBelt:Secu

3、ring the Foundations of the Rust Programming Language.In POPL 2018:ACM SIGPLAN Symposium on Principles of Programming LanguagesRalf Jung.Understanding and Evolving the Rust Programming Language.PhD dissertation,Saarland University,August 2020Recipient of the 2020 ACM Doctoral Dissertation Award Hono

4、rable MentionRecipient of the 2021 ACM SIGPLAN John C.Reynolds Doctoral Dissertation AwardRecipient of the 2021 ETAPS Doctoral Dissertation AwardRecipient of the 2021 Otto Hahn MedalRalf JungAssistant professor,Institute for Programming Languages and Systems,ETH ZrichRustBelt ProjectBackgroundIris:A

5、 Higher-Order Concurrent Separation Logic FrameworkRustBelt:Securing the Foundations of the Rust Programming LanguageCoq Proof Assistant:A Formal Proof Management Systembuilt on top ofbuilt on top ofRust Types OverviewBackgroundT&mut mut T&Tmutable borrowimmutable borrowcoercionmovemutablereborrowre

6、borrow()dropnewexclusivesharedownsborrowsHoare LogicLogicsCPreconditionPostconditionProgramGiven the precondition“P”,if we execute the program“C”and it terminates,it will hold the postcondition“Q”.PQLogicsTrue let x=10 x=10 x=3 x+=1 x=4True loop FalseHoare LogicLogicsP:x vOwnershipWe own“x”,and“x”po