Necessity Specifications for Robustness
summary
A formal language called necessity specifies robustness by stating explicit necessary preconditions: temporal-implication operators say exactly what must have held earlier for a later bad state to occur. A proof logic derives those necessity specs from ordinary functional specs (parametric over whatever verification method is used), relies on five proof ideas including encapsulation, and is mechanised in Coq. Case studies include the banking example (proved robust), the DAO reentrancy bug and ERC20-like contracts, crowdsale and DOM proxies.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:23Functional vs robustness specs
- 3:36Defining robustness
- 5:39Banking software example
- 8:54Necessity specifications semantics
- 13:29Proving necessity specs
- 18:43Soundness and encapsulation
- 20:07Case studies
- 24:42Conclusion
- 25:27Q&A
related talks
43mHolistic specifications for robust code
22mA Categorical Basis for Robust Program Analysis
19mInference of Robust Reachability Constraints
25mA Semantic Approach to Robust Property Preservation
27mUnrealizability Logic
20mOn Extending Incorrectness Logic with Backwards Reasoning
17mReasoning about External Calls
23mSpecifying and Verifying Future Conditions