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.