Pedagogical Tools for Formal Methods

在计算机科学中，形式方法是指对软件或硬件系统进行预测的数学方法。形式化方法在开发安全可靠的系统中发挥着越来越重要的作用。然而，形式化方法往往是抽象的，使用的方法和符号并不是许多计算课程的一部分。因此，有必要研究和开发有效培训网络安全学生使用正式方法的方法。目前的建议侧重于创建以编程环境为中心的教学工具。该方法将在从大学生到工业程序员的广泛人群中进行评估，以确保结果尽可能广泛适用。此外，所有产品将免费提供给其他教育工作者。本项目的主要目标是让受试者参与正式方法工具的创建，探索，推理和验证模型。重点将放在与安全相关的模型上，例如加密协议、配置、身份验证和访问控制。项目小组建议创建一系列正式语言的分级，以匹配学习进度并减少学习负担。这种方法将使学生能够使用特定领域的符号，在他们已经学习的领域的背景下采用形式化的方法。最后，它将使学生能够创建特定领域的自定义可视化，大大减少通用工具的输出与学生想要解决的问题之间的认知差距。所有这些主题都将通过实验研究和评估，以了解哪些方法是有效的，哪些是无效的。该项目得到了安全和值得信赖的网络空间（SaTC）计划的支持，该计划为解决网络安全和隐私的提案提供资金，在这种情况下，特别是网络安全教育。SATC计划与联邦网络安全研究和发展战略计划和国家隐私研究战略保持一致，以保护和维护网络系统日益增长的社会和经济效益，同时确保安全和隐私。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.