Pedagogical Tools for Formal Methods

正式方法的教学工具

• 批准号: 2208731
• 负责人: Shriram Krishnamurthi
• 金额: $ 50万
• 依托单位: Brown University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-06-01 至 2025-05-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2208731&HistoricalAwards=false
• 关键词: Pedagogical; Tools; Formal; Methods

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.

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