Pedagogical Tools for Formal Methods

Brown University, Providence RI

Investigators

Abstract

In computer science, formal methods refer to mathematical approaches to make predictions about a software or hardware system. Formal methods play an increasingly vital role in developing secure and reliable systems. However, formal methods tend to be abstract and use methods and notations that are not part of many computing curricula. As a result, there is a need to research and develop approaches to effectively train cybersecurity students to use formal methods. The current proposal focuses on creating pedagogical tools centered around programming environments. The approach will be evaluated across a broad population, from college students to industrial programmers, to ensure the results will be as broadly applicable as possible. In addition, all products will be made freely available to other educators. The primary objective of this project is to have subjects engage with formal methods tools to create, explore, reason about, and verify models. The focus will be on models related to security, such as cryptographic protocols, configuration, authentication, and access control. The project team proposes creating a series of graduated levels of formal languages to match a learning progression and reduce the learning load. This approach will enable students to use domain-specific notations to adopt formal methods within the context of domains they already study. Finally, it will enable students to create domain-specific custom visualizations that greatly reduce the cognitive gap between the output of a generic tool and the problems students want to solve. All these topics will be studied experimentally and evaluated to learn about what approaches are effective and what are not. This project is supported by the Secure and Trustworthy Cyberspace (SaTC) program, which funds proposals that address cybersecurity and privacy, and in this case specifically cybersecurity education. The SaTC program aligns with the Federal Cybersecurity Research and Development Strategic Plan and the National Privacy Research Strategy to protect and preserve the growing social and economic benefits of cyber systems while ensuring security and privacy. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.