Title: AWS re:Inforce 2024 - Verifying code using automated reasoning (APS402)

Insights:

• Introduction to Automated Reasoning: Automated reasoning is a method that uses formal logical reasoning to enhance the security, durability, availability, and overall quality of software systems. It relies on mathematical foundations to model and analyze system behavior.
• Historical Context: The roots of automated reasoning trace back to early 20th-century mathematics, with significant developments in Boolean algebra, Turing machines, and SAT solvers. These advancements laid the groundwork for modern automated reasoning tools.
• Difference from Testing: Unlike traditional testing, which can only provide partial confidence by sampling inputs, automated reasoning can exhaustively verify software behavior across all possible inputs, providing stronger guarantees.
• Automated Reasoning at Amazon: Amazon uses automated reasoning to develop and improve customer-facing products, such as CodeGuru Reviewer, Amazon Inspector, and IAM Access Analyzer. This approach helps reduce development costs and improve product quality.
• Focus on Rust: Rust is a highly desired programming language known for its safety and performance. However, unsafe Rust, which bypasses some of Rust's safety checks, requires additional verification to ensure correctness.
• Kani Tool: Kani is an open-source tool developed by Amazon for automated reasoning on Rust code. It verifies properties like memory safety, absence of overflow, and custom assertions, particularly in unsafe Rust code.
• User Stories: Examples include s2n-quic, which uses Kani to verify performance optimizations, and Firecracker, which uses Kani to ensure VM separation and traffic rate limiting.
• Proof-Guided Development: This approach involves writing proof harnesses and properties before implementing functions, allowing developers to verify correctness throughout the development process.
• Debugging with Kani: Kani provides counterexamples with concrete input values that reveal bugs, allowing developers to debug and correct their code effectively.
• Limitations and Future of Kani: Kani has limitations, such as handling floating-point operations, long-running loops, and concurrent code. However, Amazon is committed to improving Kani and using it to verify critical parts of the Rust standard library.

Quotes:

• "Automated reasoning focuses on the automation of formal logical reasoning to raise the bar on the security, the durability, availability, and overall quality and correctness of systems, software systems."
• "Automated reasoning doesn't look at historical data of a system to predict future behavior. We're really using formal models of the system and we're analyzing the models to prove the correctness of the model and hence of the software that's modeled."
• "Most software is too complex to be exhaustively tested. And that's what automated reasoning provides an answer for."
• "Rust is one of the, or if not the fastest growing language inside of Amazon. We have multiple services and applications adopting Rust or being ported to Rust."
• "Kani lets you verify unsafe code blocks in Rust. So all these raw pointer manipulations, unchecked arithmetic operations, Kani has your back if you use the tool for that kind of software."
• "Proof harnesses are very similar to traditional test harnesses, they look the same and they're very simple to write but when you start using this you have a very like higher return on investment for your time."
• "If you're using unsafe rust and you're not using Kani, you have no excuse either because unsafe rust, everything rests on you as a developer to enforce correctness and make sure you don't break all the guarantees that safe Rust provides."
• "Kani is actively developed and supported. We're working on adding new features that enable better scalability, like compositional reasoning, stubbing functions out with abstract models to scale verifications, function contracts, loop contracts to go beyond the unwinding we do and do unbounded reasoning on loops."
• "Please give Kani a try. It's gonna take you some, maybe a day or two to get used to the way of thinking about proofs but you're really gonna get some nice results on your code."