How Amazon Web Services Uses Formal Methods (2015) [pdf]
cslab.pepperdine.edu
How Amazon Web Services Uses Formal Methods (2015) [pdf]
1–10 of 30 posts
Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]
#2A thread from 2014, presumably pre-publication:
https://news.ycombinator.com/item?id=8096185
A bit more: https://news.ycombinator.com/item?id=9289890
Related from 2015: https://news.ycombinator.com/item?id=9287426
Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]
#3I’ve started using TLA+ in my spare time. There are several good sites and books to learn more about it:
- https://learntla.com/introduction/
- Pracitcal TLA+
It’s much easier to get running with than other formal methods tools like Isabelle and Coq.
Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]
#4I’ve started using TLA+ in my spare time. There are several good sites and books to learn more about it: - https://learntla.com/introduction/ - Pracitcal TLA+ It’s much easier to get running with than other formal methods tools like Isabelle and Coq.
I recommend "Practical TLA+" too; it introduces TLA+ in a more approachable way than other resources.
Link to the book: https://www.apress.com/gp/book/9781484238288
Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]
#5Bryon Cook, a principal scientist at Automated Reasoning Group gives an overview of various solvers in-use today at AWS: https://www.youtube.com/watch?v=UKqVY0SSbus
Here's a presentation by Eric, a distinguished engineer, and Neha, a principal engineer, on analysing IAM policies (Zelkova?) and Network reachability (Tiros?): https://www.youtube.com/watch?v=x6wsTFnU3eY
This webpage has many more links to blog articles on the topic: https://aws.amazon.com/security/provable-security/
Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]
#6I introduced TLA+ to help understand underlying components in the OpenStack ecosystem and at small companies to solve thorny problems. It's well worth learning as it gives you a very different perspective on the design and construction of systems.
In addition to the books and sites mentioned here, there's also a video course with tutorial content produced by the creatore of TLA+: https://lamport.azurewebsites.net/video/videos.html
Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]
#7I introduced TLA+ to help understand underlying components in the OpenStack ecosystem and at small companies to solve thorny problems. It's well worth learning as it gives you a very different perspective on the design and construction of systems. In addition to the books and sites mentioned here, there's also a video course with tutorial content produced by the creatore of TLA+: https://lamport.azurewebsites.net/vid…
Hey! It sounds like you're using TLA+ in a consulting style role within small companies? How did you manage to get into that?
Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]
#8I introduced TLA+ to help understand underlying components in the OpenStack ecosystem and at small companies to solve thorny problems. It's well worth learning as it gives you a very different perspective on the design and construction of systems. In addition to the books and sites mentioned here, there's also a video course with tutorial content produced by the creatore of TLA+: https://lamport.azurewebsites.net/vid…
Hey! It sounds like you're using TLA+ in a consulting style role within small companies? How did you manage to get into that?
I double on this question
Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]
#9Bryon Cook, a principal scientist at Automated Reasoning Group gives an overview of various solvers in-use today at AWS: https://www.youtube.com/watch?v=UKqVY0SSbus Here's a presentation by Eric, a distinguished engineer, and Neha, a principal engineer, on analysing IAM policies (Zelkova?) and Network reachability (Tiros?): https://www.youtube.com/watch?v=x6wsTFnU3eY This webpage has many more links to blog articles…
Yes, since we published this (I'm one of the authors), the Automated Reasoning Group have done amazing work applying formal methods to a broad range of problems at AWS. We're also still using TLA+ in many places for the reasons the paper describes.
One aspect of TLA+ (and formal specifications in general) that I under appreciated when we wrote this was how useful they are as a communication tool. I've found well-commented TLA+ to be an excellent medium for reviewing and documenting protocols, and having high-bandwidth conversations about them. Complex protocol interactions can be hard to describe clearly in text, but the mix of text and TLA+ (or PlusCal) seems to work well.
Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]
#10I’ve started using TLA+ in my spare time. There are several good sites and books to learn more about it: - https://learntla.com/introduction/ - Pracitcal TLA+ It’s much easier to get running with than other formal methods tools like Isabelle and Coq.
Practical TLA+ is indeed a great place to start, and Hillel Wayne's writing out formal methods is all worth reading.
Lamport's TLA+ book, and "Specifying Systems" are both available online (https://lamport.azurewebsites.net/tla/book.html). That one's worth a read too. Lamport's approach to teaching TLA+ is different, and probably more suited to the mathematically-inclined.
If you like spelunking through history, I'd also recommend checking out some of Lamport's papers on TLA. I particularly like "What Good is Temporal Logic?" which lays out his early arguments about why temporal logic is useful for solving some classes of problems. The paper is available here: https://www.microsoft.com/en-us/research/uploads/prod/2016/1...