CRII: SHF: A New Foundation for Attack Trees Based on Monoidal Categories

CRII：SHF：基于幺半群类别的攻击树的新基础

• 批准号: 1565557
• 负责人: Harley Eades
• 金额: $ 7.03万
• 依托单位: AUGUSTA UNIVERSITY RESEARCH INSTITUTE, INC.
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-03-01 至 2019-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1565557&HistoricalAwards=false
• 关键词: CRII; SHF; New; Foundation; Attack

Title: CRII:SHF: A New Foundation for Attack Trees Based on Monoidal Categories Attack trees are a modeling tool used to assess the threat potential of a security critical system. They have been used to analyze the threat potential of the cybersecurity of power grids, wireless networks, and many others. Attack trees for real-world security scenarios can grow to be quite complex and manipulating such large and complex trees without a formal semantics can be dangerous. The intellectual merits of the research are twofold: 1) It develops, using the power of linear logic and category theory, a new mathematical semantics of attack trees that is more general than existing models; 2) It designs a new domain-specific programming language for conducting threat analysis using attack trees. The language is specifically designed for not only the construction and manipulation of attack trees, but also for the ability to verify properties of attack trees. The project's broader significance and importance are improvement of security and reliability of software, training of a diverse group of undergraduate students at Georgia Regents University in principles of programming languages and security, and exposing them to research.The project's first step is to give attack trees a categorical semantics in symmetric monoidal categories. Then based on this semantics, and the connection between linear logic and symmetric monoidal categories, the project develops a newstatically-typed linear functional programming language called Lina (Linear Threat Analysis). Types in Lina correspond to attack trees, and programs between attack trees correspond to semantically valid transformations of attack trees. Therefore, designing and manipulating complex attack trees in Lina provides a higher confidence that the resulting analysis is correct.

标题：CRII：SHF：基于单一类别的攻击树的新基础攻击树是用于评估安全关键系统的威胁潜力的建模工具。它们已被用于分析电网、无线网络和许多其他网络安全的潜在威胁。现实世界安全场景的攻击树可能会变得非常复杂，在没有正式语义的情况下操作如此庞大和复杂的树可能是危险的。该研究的智力价值有两个方面：1)它利用线性逻辑和范畴理论的力量，开发了一种新的攻击树的数学语义，比现有的模型更具一般性；2)它设计了一种新的特定于领域的编程语言，用于使用攻击树进行威胁分析。该语言不仅专为构建和操作攻击树而设计，而且还专为验证攻击树的属性而设计。该项目的更广泛的意义和重要性是提高软件的安全性和可靠性，对佐治亚州摄政大学的一群不同的本科生进行编程语言和安全原理的培训，并让他们进行研究。该项目的第一步是在对称的单体类别中为攻击树提供分类语义。然后基于这种语义，以及线性逻辑和对称么半群范畴之间的联系，本项目开发了一种新型的静态类型的线性函数式程序设计语言LINA(线性威胁分析)。LINA中的类型对应于攻击树，而攻击树之间的程序对应于攻击树的语义有效转换。因此，在LINA中设计和操作复杂的攻击树可以更好地确保分析结果的正确性。