FMitf 2024 HOME Current PIs Aspiring PIs;ORGANIZATION
Invited Speakers
Speaker: Emina Torlak (AWS)
Title: Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (slides)
Abstract:
Authorization is the problem of deciding who has access to what in a multi-user system. Every cloud-based application has to solve this problem, from photo sharing to online banking to health care. This talk presents Cedar, a new language for authorization that is designed to be ergonomic, fast, safe, and analyzable. Cedar’s simple and intuitive syntax supports common authorization use-cases with readable policies, naturally leveraging concepts from role-based, attribute-based, and relation-based access control models. Cedar’s policy structure enables authorization requests to be decided quickly. Its policy validator leverages optional typing to help policy writers avoid mistakes, but not get in their way. Cedar’s design has been finely balanced to allow for a sound and complete logical encoding, which enables precise policy analysis, e.g., to ensure that when refactoring a set of policies, the authorized permissions do not change. We have implemented Cedar in Rust and used Lean to formally verify important properties of its design. Cedar is used at scale in Amazon Verified Permissions and Amazon Verified Access, and it is freely available here.
Bio:
Emina Torlak is a Senior Principal Scientist at Amazon Web Services and was previously an Associate Professor at the University of Washington. Emina works on new languages and tools for program verification and synthesis. She received her Bachelors (2003), Masters (2004), and Ph.D. (2009) degrees from MIT. Emina is the creator of Rosette and Kodkod and leads the development of Cedar. Rosette is a solver-aided language that powers verification and synthesis tools for all kinds of systems, from radiation therapy control to Linux JIT compilers. Kodkod is a solver for relational logic, used widely in tools for software analysis and design. Cedar is an expressive, fast, and analyzable language for authorization, applied at scale in Amazon Verified Permissions and AWS Verified Access. Emina is a recipient of the Robin Milner Young Researcher Award (2021), NSF CAREER Award (2017), Sloan Research Fellowship (2016), and the AITO Dahl-Nygaard Junior Prize (2016).
Speaker: Aaron Dutle (NASA)
Title: Formal Methods in the Air (slides)
Abstract:
This talk will discuss some of the successes that NASA Langley has experienced in the development and application of Formal Methods. We will consider the development of the Well-Clear definition for uncrewed aircraft and the subsequent creation of the DAIDALUS Detect and Avoid library, and how this led to the team's work on the Compact Position Reporting algorithm, and eventually to the development of PRECiSA and ReFlow, a pair of tools for floating-point analysis.
Bio:
Dr. Aaron Dutle is a Research Computer Scientist in the Safety-Critical Avionics Systems branch at NASA Langley Research Center. His primary research is in the development of Formal Methods and their application to aerospace systems, specifically the use of Interactive Theorem Proving. He holds a PhD in mathematics from the University of South Carolina, and his Erdős number is 2.
Speaker: Grant Passmore (Imandra)
Title: Formal Verification of Financial Infrastructure with Imandra (slides)
Abstract:
Many deep issues plaguing today’s financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Imandra, we have pioneered the application of formal verification to financial markets, and firms like Goldman Sachs, Itiviti and OneChronos rely upon Imandra’s algorithm governance tools for the design, regulation and calibration of many of their most complex algorithms. With a focus on financial infrastructure (e.g., the matching logics of national exchanges and dark pools), we will describe the landscape and illustrate our Imandra system on a number of real-world examples. We’ll sketch open problems and future directions along the way.
Bio:
Grant Passmore is co-founder and Co-CEO of Imandra Inc. Grant is a widely published researcher in formal verification and symbolic AI, and has more than fifteen years’ industrial formal verification experience. He has been a key contributor to safety verification of algorithms at Cambridge, Carnegie Mellon, Edinburgh, Microsoft Research and SRI. He earned his PhD on automated theorem proving in algebraic geometry from the University of Edinburgh, is a graduate of UT Austin (BA in Mathematics) and the Mathematical Research Institute in the Netherlands (Master Class in Mathematical Logic), and is a Life Member of Clare Hall, University of Cambridge.
Speaker: Joe Kiniry (Galois)
Title: Scaling Formal Methods in the Field at Galois (slides)
Abstract:
Galois is known for doing formal methods R&D. A lot of formal methods R&D. In every project—and we run around fifty at once—we are asked to create a new programming, specification, or domain-specific language, a new interpreter or compiler, a new verification tool, a new user experience, a new-to-the-world capability. While this is fun, it is also a bit exhausting.
This is, in part, because a company of 100+ formal methods geeks can only do so much. We can only build, fix, or improve as many new and existing systems with formal methods as there are hours in the day, performers available to work, and butts in seats.
This talk is about that limitation, and our force multipliers for putting formal methods in the field: (1) creating domain-specific spinouts to make our impact more “real”, (2) training the trainers to spread knowledge, (3) putting applied formal methods tools in the hands of everyday engineers, often “behind the scenes,” and (4) creating reusable, maintainable, evolvable assets into real product lines and platforms.
Bio:
Dr. Joe Kiniry has been a Principal Scientist at Galois for 10 years. He is also the Principled CEO and Chief Scientist of the public benefit corporation Free & Fair. He was previously an academic in Europe for twelve years, lastly as a Full Professor and Head of Section at the Technical University of Denmark. Joe has extensive experience in formal methods, the foundations of mathematics, information security, and high-assurance, model-based software, firmware, hardware, safety, security, requirements, and systems engineering—what we now call Rigorous Digital Engineering at Galois. He has over twenty years experience in the design, development, assurance, support, and auditing of nationally critical, safety-critical, and national security systems, including supervised and internet/remote electronic voting systems. Joe has served as an adviser to the Dutch, Irish, Danish, and US governments in matters relating to electronic voting. He holds a PhD from the California Institute of Technology.