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

职务名称：CRII：SHF：基于Monoidal范畴的攻击树的一种新构造攻击树是一种用于评估安全关键系统潜在威胁的建模工具。 它们已被用于分析电网，无线网络和许多其他网络安全的潜在威胁。 现实世界安全场景的攻击树可能会变得非常复杂，在没有正式语义的情况下操纵如此庞大而复杂的树可能是危险的。 该研究的智力价值是双重的：1）它开发，使用线性逻辑和范畴理论的力量，一个新的数学语义的攻击树，这是更一般的比现有的模型; 2）它设计了一个新的特定于域的编程语言进行威胁分析使用攻击树。该语言是专门设计的，不仅用于攻击树的构造和操作，而且还能够验证攻击树的属性。该项目的更广泛的意义和重要性是提高软件的安全性和可靠性，培训格鲁吉亚摄政大学的一批不同的本科生，使他们了解编程语言和安全性的原则，并使他们接受研究。然后，基于这种语义，以及线性逻辑和对称monoidal范畴之间的联系，该项目开发了一种新的静态类型的线性函数编程语言，称为Lina（线性威胁分析）。Lina中的类型对应于攻击树，攻击树之间的程序对应于攻击树的语义有效转换。 因此，在Lina中设计和操作复杂的攻击树可以更好地确保分析结果的正确性。

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.