CAREER: SAIF: Security Assurance through AI and Formal Approaches for System-on-Chips

集成电路是许多重要电子设备和系统的关键组件，包括用于金融服务、军事和国防应用、医疗保健系统和商业运营的设备和系统。这类电路由于其复杂的功能、大量功能块之间的交互增加以及与互联网的连接，因此受到越来越多的安全漏洞和攻击。此类电路的任何安全和信任要求的失败都可能导致敏感信息泄露、侵犯隐私、关键基础设施损坏，并可能危及人类生命。因此，检查这种复杂电路的安全性是至关重要的，但同时也具有挑战性，因为它需要创新的解决方案来应对复杂性、大量的安全漏洞和各种攻击方法。该项目开发了一个名为SAIF的创新人工智能(AI)辅助安全验证框架，以解决以下目标：(I)提供高验证覆盖率，(Ii)通过将人类排除在过程之外，将安全验证时间缩短数量级，(Iii)提供电路复杂性的可扩展性，以及(Iv)提供对新攻击面的适应性。SAIF为设计和验证工程师提供了在制造之前检查安全漏洞的属性和工具。SAIF使用AI开发安全属性和规则的综合数据库，支持功能安全属性生成，辅助安全规则生成和验证，并促进用于安全验证和验证的AI测试生成。该项目将整合研究和教育活动，为高中生、劳动力发展、少数族裔招募、K-12和本科生的培训/讲习班制定修订的课程/教学大纲，并通过出版物、研讨会、教程和小组讨论来传播研究成果。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Integrated circuits are critical components in many vital electronic devices and systems, including those used in financial services, military and defense applications, healthcare systems, and business operations. Such circuits are subject to an ever-growing number of security vulnerabilities and attacks due to their complex functionality, increased interactions among numerous functional blocks, and connectivity to the internet. Any failure of security and trust requirements of such circuits can lead to sensitive information leakage, privacy violations, critical infrastructure damage, and potentially endanger of human life. Examining the security of such complex circuits is therefore critical, but at the same time challenging, in that it requires innovative solutions to tackle complexity, a large number of security vulnerabilities, and various methods of attack. This project develops an innovative artificial intelligence (AI)-assisted security verification framework called SAIF to address the following objectives: (i) provide high verification coverage, (ii) lower security verification time by orders of magnitude by taking humans out of the process, (iii) provide scalability of circuit complexity, and (iv) offer adaptability to new attack surfaces. SAIF provides the design and verification engineers with properties and tools to check for security vulnerabilities before fabrication. SAIF uses AI to develop a comprehensive database of security properties and rules, support functional security property generation, assist security rule generation and verification, and facilitate AI- test generation for security verification and validation. This project will integrate research and educational activities by developing a modified curriculum/syllabus for high schoolers, workforce development, minority recruiting, training/workshops for K-12 and undergraduate students, and disseminating research results through publications, seminars, tutorials, and panels.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.