Formal Methods at Scale

In Fall 2019 the National Science and Technology Council's Special Cyber Operations Research and Engineering Subcommittee convened two one-day meetings to discuss successes and barriers, opportunities and challenges, in the (accelerating) use of formal methods in cyber systems. The one-day meetings brought together a by-name group of experts to discuss technical areas to include formal methods logics, tools, and ecosystems, as well as to consider more broadly their related evaluation and use. Ultimately the meeting discussions and summary reporting is meant to encourage understanding of how the formal methods community might achieve the use of this critical technology at scale.

We recognize that there are multiple dimensions of scale that we will need to address. These include, for example: (1) the range of properties and qualities that are modeled and reasoned about, such as relating to security, safety, performance, fault tolerance, real-time, etc., (2) complexity and the size of systems and their supply chains, including issues related to composability (3) efficiency of FM-related modeling, tooling, and engineering practices, including integration into mainstream tooling and practices, (4) ability to rapidly co-evolve systems and associated evidence, (5) ease of use for non-expert developers and evaluators.

We are also interested in addressing the different dimensions of experience that we can share. Discussion of these experiences can help ground our conversation, and help us understand cross-cutting considerations such as commonalities in technical foundations, and challenges relating to adoption into practice and tooling. Some kinds of experiences we can share include: (1) applications to specific major systems in government and industry, (2) tour-de-force results, such as proofs of significant mathematical results or reasoning about modern processors, (3) the advancement of formal methods ecosystems surrounding the various provers and stacks, (4) integration of more limited capabilities into broader communities of practice, such as has been happening in major tech firms.

FM@Scale East was held on September 25, 2019 at SRI International in Arlington, Virginia. FM@Scale West was held on October 9, 2019 at SRI Menlo Park.

If you have any questions, please contact the organizers: FMatScale@cps-vo.org

Meeting Sponsor
Brad Martin

Co-Chairs

Patrick Lincoln, SRI International
William Scherlis, Carnegie Mellon University

Patrick Lincoln, Ph.D., is director of the Computer Science Laboratory at SRI International. He is also the executive director of SRI's program for the Department of Homeland Security’s Cyber Security Research and Development Center and director of the SRI Center for Computational Biology. Lincoln leads research in the fields of formal methods, computer security and privacy, computational biology, scalable distributed systems, and nanoelectronics.

He has led multidisciplinary groups conducting high-impact research projects in symbolic systems biology, scalable anomaly detection, exquisitely sensitive biosensor systems, strategic reasoning and game theory, and privacy-preserving data sharing. He has published dozens of influential papers, holds several patents, has served on scientific advisory boards for private and publicly held companies, nonprofits, and government agencies and departments.

Lincoln holds a Ph.D. in computer science from Stanford University and a B.Sc. in computer science from MIT. He has previously held positions at MCC, Los Alamos National Laboratory, and ETA Systems.

Lincoln was named an SRI Fellow in 2005.

William L. Scherlis is a Professor of Computer Science and director of CMU's Institute for Software Research (ISR), one of seven academic departments in the School of Computer Science (SCS). ISR research and educational programs relate to software development, cybersecurity, privacy engineering, Internet of Things, network analysis, mobility, systems assurance, and other topics. ISR is home to two PhD programs and three professional Masters programs. Scherlis founded the PhD Program in Software Engineering in 1999 and directed it for more than a decade. During 2012 and early 2013 he was the Acting CTO for the Software Engineering Institute, a Department of Defense FFRDC at CMU.

Scherlis joined the Carnegie Mellon faculty after completing an A.B. magna cum laude at Harvard University in applied mathematics, a year in the Department of Artificial Intelligence at the University of Edinburgh (Scotland) as a John Knox Fellow, and a Ph.D. in computer science at Stanford University (Zohar Manna advisor). His research relates to software assurance, cybersecurity, software analysis, and assured safe concurrency. His team has developed analysis tools based on techniques to verify safe concurrency, information flow, and other properties that tend to defy conventional testing and heuristic analysis. He has led several large research projects including the National Security Agency Science of Security Lablet at CMU since its inception in 2011 and, previously, the Carnegie Mellon / NASA High Dependability Computing Project (HDCP).

Scherlis has testified before Congress on federal software sustainment, on computing technology and innovation, and on roles for a Federal CIO. He interrupted his career at CMU to serve at Defense Advanced Research Projects Agency (DARPA) for more than six years, departing in 1993 as a federal senior executive. At DARPA his responsibilities related to research and strategy in software technology, computer security, information infrastructure, and other topics. He participated in the initiation of the high performance computing and communications (HPCC) program (now NITRD) and in defining the concept for CERT-like security organizations, hundreds of which now operate in more than 90 countries world-wide.

Scherlis has led multiple national studies including the National Research Council (NRC) study committee that produced the report Critical Code: Software Producibility for Defense in 2010. He served multiple terms as a member of the DARPA Information Science and Technology Study Group (ISAT). He has been an advisor to major technology firms, defense companies, and venture investors, and is a co-founder of Panopto, a CMU spin-off. He has served as program chair for a number of technical conferences including the ACM Foundations of Software Engineering (FSE) Symposium and the ACM Symposium on Partial Evaluation and Program Manipulation (PEPM).

He is a Fellow of the IEEE and a Lifetime National Associate of the National Academy of Sciences.