Systems Software Verification Summer School
In this chapter, delve into advanced refinement concepts presented by experts from the University of Michigan and VMWare Research. Explore topics like refinement recap, verification checks, interpretation functions, modeling network constraints, and more.
Uploaded on Feb 15, 2025 | 0 Views
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Systems Software Verification Summer School Chapter 9 Chapter 9 Advanced Refinement Advanced Refinement Manos Kapritsos, University of Michigan Jon Howell, VMWare Research Rob Johnson, VMWare Research
REFINEMENT RECAP function I(ds:DS) : SpecState { } predicate Inv(ds:DS) { } Spec lemma Refinement(ds, ds ) ensures Init(ds) SpecInit(I(ds)) && Inv(ds) ensures Next(ds, ds ) && Inv(ds) SpecNext(I(ds), I(ds )) && Inv(ds ) Distributed system Host Network Host Host
code the verifier checks for you code you need to inspect Spec Distributed system Host Network Host Host Build system
code the verifier checks for you code you need to inspect Spec Q: Can the interpretation function Interp() be a *.i.dfy file? Distributed system Host Network Host Host *.s.dfy *.i.dfy
What if the interpretation function pretended nothing ever happened? function Interp(ds:DS) : SpecState { var a0 :| SpecInit(a0); a0 } Always returns the initial state predicate Inv(ds:DS) { true }
or just made up a fake story? datatype DistState = DistState(actualState: Stuff, fakeState: HostState) function Interp(ds:DS) : SpecState { ds.fakeState } Returns fake state
Maybe trusting function Interp() isnt the best idea Make it Interp. Interp.s.dfy s.dfy and have an examiner examine it ugh, that s a bad idea! The examiner would have to read the entire protocol description
MESSAGE CORRESPONDENCE Idea: let s leverage the fact that the Network is Idea: let s leverage the fact that the Network is trusted to constrain function trusted to constrain function Interp() Model user-visible messages (requests or replies) in the application spec Demand a proof that user-visible messages on the network correspond to spec-level state I.e. show that the following predicate holds at all times Message_Correspondence(protocolState:ProtocolState, specState:SpecState) Function Interp() is no longer trusted. It is just part of the proof that constructs specState as Interp(protocolState)
MESSAGE CORRESPONDENCE Spec S4 S3 S1 S2 S0 I0 I1 I2 I3 I4 Implementation/protocol
EXAMPLE: PAXOS Spec (serviceState) takes in serviceState.requests, executes them and produces serviceState.replies predicate Message_Correspondence(concretePkts:set<LPacket<EndPoint, seq<byte>>>, serviceState:ServiceState) { && (forall p, seqno, reply :: && p in concretePkts && p.src in serviceState.serverAddresses && p.msg == MarshallServiceReply(seqno, reply) ==> AppReply(p.dst, seqno, reply) in serviceState.replies) && (forall req :: req in serviceState.requests ==> exists p :: && p in concretePkts && p.dst in serviceState.serverAddresses && p.msg == MarshallServiceRequest(req.seqno, req.request) && p.src == req.client) } Your spec state produced the corresponding reply Reply message in network Corresponding request message must be in the network (from that client) Your spec state received the corresponding request
APPLICATION CORRESPONDENCE Spec S4 S3 S1 S2 S0 I0 I1 I2 I3 I4 Implementation/protocol In Distributed Systems we use messages to define correspondence, but the idea is generalizable to other kinds of events
