Reasoning about Deltas — Even Doing Nothing is Difficult
| Abstract: Formal software verification involves specifications, an implementation, and a proof that the implementation satisfies the specifications. When an actively-developed implementation evolves, the typical approach is to update the formal specifications and proof accordingly. The old version of specifications is simply relegated to history without attempting to formally relate the old and new versions. This approach is inefficient when the implementation changes to expand on input datatypes while retaining the functionality for legacy inputs. Such implementation changes produce comparable old and new specifications, we propose to formally relate and prove properties about the comparable specifications. A formal relation between comparable specifications could enable the proof engineers to utilize the existing proof infrastructure for proving backward compatibility. |
We call this process proof evolution: a technique for identifying and relating similarities and changes between comparable specifications and proofs. In this talk, I will present the active development of automated tools for enabling and facilitating proof evolution within Amazon Web Services (AWS).
A particular use case, that has motivated the need of automated tools for proof evolution, occurs at AWS Identity [1]. AWS authenticates and authorizes over 34 trillion requests per day [2]. AWS Identity has a custom language for specifying access control policies and a corresponding authorization engine that determines access rights for each request by evaluating the relevant policies. We use Dafny, a verification-aware programming language, to verify that the authorization implementation satisfies the intended specifications. When there are changes to the policy language and actively-developed Java implementation, proof engineers at AWS are required to manually update Dafny specifications and the corresponding proofs. To help streamline this process, we propose that the specifications and proofs evolve alongside the code.
We identify that quite often proof engineers initiate changes to existing specifications by altering types of objects by removing, augmenting and/or introducing new types. To prove properties between such comparable specifications, a conventional approach is to keep the old and new versions around, and manually build injections (mapping functions) between types within the two versions. The type injections provide the necessary infrastructure for proving properties of interest between the comparable specifications. To reduce the manual effort involved, we have developed and open-sourced an analysis tool called typeCart (name-blend of type and cartography) [3]. typeCart automatically identifies equivalent and inequivalent types between comparable specifications, and generates injections for the equivalent types. The generated injections i) mechanically relate the comparable specifications, ii) remove the need of keeping the two versions of specification around and iii) help proof engineers for proving backward compatibility for specifications. To achieve trustworthiness for the injections, typeCart generates verification contracts for the injections, enabling the Dafny verifier to automatically discharge verification conditions of the generated type injections.
We are evolving typeCart to equip proof engineers with automated tools to prove compatibility between specifications when we introduce new types and augment existing types. We plan to implement workflows for typeCart integration with the version control system of Dafny-based developments at AWS, and its instrumentation to varying codebases of comparability and size.
Hira Syeda is an Applied Scientist II in Amazon Web Services (AWS) Identity, working on formal verification techniques for cloud security. Prior to joining AWS, Hira worked as a postdoctoral researcher at Chalmers University of Technology in Sweden, implementing verified compilers for cyber-physical systems. Hira completed her PhD research, in 2019, at UNSW Australia and with the Trustworthy Systems group, Data61 CSIRO. Her PhD research is related to low-level program verification and interactive theorem proving.
[1] https://aws.amazon.com/identity/
[2] https://aws.amazon.com/blogs/aws/happy-10th-birthday-aws-identity-and-accessmanagement/
[3] https://github.com/awslabs/typecart