Speakers

Darren Cofer

Darren Cofer is a Principal Fellow at Collins Aerospace. He earned his PhD in Electrical and Computer Engineering from The University of Texas at Austin. His area of expertise is developing and applying advanced analysis methods and tools for verification and certification of high-integrity systems. He is currently leading the Collins team on DARPA’s PROVERS program, developing and applying formal methods for verification of safety and security properties in autonomous air vehicles. He served on RTCA committee SC-205 developing new certification guidance for airborne software (DO-178C) and was one of the developers of the Formal Methods Supplement (DO-333). He is currently a member of SAE committee G-34 developing certification guidance for the use of machine learning technologies onboard aircraft.

AI in the Sky (and how formal methods will get us there safely)

AI and ML are dominating headlines, boardrooms, social media, and computing research with promises of a utopian future of unimaginable productivity and scientific breakthroughs -- or possibly the end of humanity. But when we cut through the hype, there are real engineering problems to be solved before we reach the promised land. Suppose we want to use machine learning technologies onboard aircraft. The reasons for doing so range from increasing autonomy and easing pilot workload, to simply reducing the computing resources required by avionics. Can these benefits be realized while maintaining or even improving aircraft safety? What are the barriers and how might they be overcome? Researchers, regulators, and the aviation industry have been working to answer these questions, developing new guidance for certification of ML-based airborne systems and creating new technologies and processes for meeting those certification objectives and satisfying safety requirements. Formal methods will play a large role in how we put AI in the sky, safely.

Emina Torlak

Emina Torlak is a Senior Principal Scientist at Amazon Web Services and an Affiliate 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, used at scale at Amazon Web Services and beyond. 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).

Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization

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 by reduction to SMT. Cedar’s simple and intuitive syntax supports common authorization use-cases with readable policies, naturally expressing 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 uses 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, complete, and decidable logical encoding, which enables precise policy analysis, e.g., to ensure that policy refactoring preserves existing permissions. 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 at https://github.com/cedar-policy.

Natasha Neogi

Dr. Natasha Neogi is Senior Technologist for Assured Intelligent Flight Systems at NASA, and a Senior Researcher at the NASA Langley Research Center. Her primary research interests are in the verification and validation of software-intensive safety-critical infrastructure systems, as well as certification issues concerning airworthiness of non-conventionally piloted vehicles. Previously, she was a staff scientist in the Office of the Chief Scientist, NASA Headquarters. She received her Ph.D in Aeronautical and Astronautical Engineering from the Massachusetts Institute of Technology. She is a fellow of the AIAA and was the recipient of the AIAA Robert A. Mitcheltree and PEC Doug P. Ensor Young Engineer awards as well as NASA’s 2021 Outstanding Leadership Medal. She has numerous awards and publications in AIAA, IEEE and ACM conferences and journals.

Paul Miner

Dr. Paul Miner is a Senior Research Engineer at NASA Langley Research Center, and currently the Project Scientist on the System-Wide Safety project. He is a sought-after subject matter expert in aviation safety and formal methods, having worked on multiple NASA, FAA, and DARPA projects. He has conducted research in state-of-the-art design and verification methods for digital avionics where he has developed new, innovative methods for formally verifying digital hardware and software used in high-integrity mission- and safety-critical systems. He has integrated these methods with standard engineering environments to facilitate technology transfer to industry and the FAA and has led the development of novel architectures and algorithms to provide new capabilities for digital system survival in the presence of multiple environmentally induced faults. Dr. Miner received his Ph.D in Computer Science from Indiana University, and his Master’s degree in Computer Science from William & Mary.

Page last update: September 2024

NASA Official: César Muñoz

LaRC Privacy Statement