Back.
Public information on Automated Reasoning at Amazon as of Sept 2021:
- Apply for internships!
- Amazon Research Awards
- Websites with information:
- Staff scientists at "Principal", "Senior Principal", or "Distinguished" level (see levels.fyi for comparisons):
-
Andrew Gacek,
-
Bor-Yuh Evan Chang (Part-time),
-
Bruno Dutertre,
-
Byron Cook,
-
Cesar Munoz,
-
Daniel Kroening,
-
Dimitra Giannakopoulou,
-
Emina Torlak,
-
Ernie Cohen,
-
Franco Raimondi (Part-time),
-
Jaco Geldenhuys,
-
Jared Davis,
-
Jim Grundy,
-
John Harrison,
-
Ken McMillan (Part-time),
-
Lee Pike,
-
Marijn Heule (Part-time),
-
Mark Tuttle,
-
Mike Hicks,
-
Mike Whalen,
-
Murat Demirbas,
-
Nathan Chong,
-
Neha Rungta,
-
Niko Matsakis,
-
Rajeev Joshi,
-
Remi Delmas,
-
Rupak Majumdar (Part-time),
-
Rustan Leino,
-
Serdar Tasiran,
-
Suresh Jagannathan (Part-time),
-
Teme Kahsai,
-
Willem Visser,
-
Xi Wang (Part-time),
-
Zvonimir Rakameric.
Note that I am only listing staff that have listed their affiliation on
public websites such as
LinkedIn, Google scholar, amazon.science, or univeristy websites. We have
some senior staff who have choosen to keep their affiliation private.
- Papers
- Using lightweight formal methods to validate a key value storage node in Amazon S3, SOSP'21
- Formally verifying FreeRTOS' interprocess communication mechanism, Embedded World '21
- Pre-deployment security assessment for cloud services through semantic reasoning, CAV'21
- Verified cryptographic code for everybody, CAV'21
- Debugging network reachability with blocked paths, CAV'21
- Code-level model checking in the software development workflow at Amazon Web Services, ICSE'21
- Using model checking tools to triage the severity of security bugs in the Xen hypervisor, FMCAD'20
- RAPID: checking API usage for the cloud in the cloud, ESEC'21
- Stratified abstraction of access control policies, CAV'20
- IDE support for cloud-based static analysis, ESEC'20
- Continuous compliance, ASC'20
- Verifying object construction, ICSE'20
- Block public access: Trust safety verification of access control policies, ESEC'20
- Reachability Analysis for AWS-based Networks, CAV'19
- Object-oriented security proofs, FM'18
- Formal reasoning about the security of Amazon Web Services, CAV'18 Invited paper
- Model-checking boot code from AWS datacenter, CAV'18
- Semantic-based Automated Reasoning for AWS Access Policies using SMT, FMCAD'18
- Continuous formal verification of Amazon s2n, CAV'18
- SideTrail: Verifying Time-Balancing of Cryptosystems, VSTTE'18
- Practical Methods for Reasoning about Java 8's Functional Programming Features, VSTTE '18
- Interviews:
- Lectures by AWS customers:
- Lectures aimed at customers and industry:
- Talks aimed at science community:
- The business of proof, Workshop on Dependable and Secure Software Systems 2021
- How I learned to stop worrying and start applying automated reasoning, FACC'21 (other relevant talks at FACC website)
- Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning, CAV'21
- Verified Cryptographic Code for Everybody, CAV'21
- Debugging Network Reachability with Blocked Paths, CAV'21
- Embedded World 2021: Formally Verifying the FreeRTOS IPC Mechanism, Embedded World '21
- Stratified abstraction of access control policies, CAV'20
- Formal reasoning about the security of Amazon Web Services, FLoC 2018 plenary lecture
- Formal reasoning about the security of Amazon Web Services, OOPSLA/SPLASH 2018 keynote lecture
- (skip to 30mins in): SideTrail: Verifying Time-Balancing of Cryptosystems
- What is Automated Reasoning? How Is it Used at AWS?,
- Provable Security at AWS, USENIX Enigma 2019
- On automated reasoning for compliance certification, CAV workshop on Formal Approaches to Certifying Compliance (FACC)
- Blog posts and informational videos
- Press:
Back.