EnnCore: End-to-End Conceptual Guarding of Neural Architectures

EnnCore：神经架构的端到端概念防护

• 批准号: EP/T026995/1
• 负责人: Lucas Cordeiro
• 金额: $ 219.36万
• 依托单位: University of Manchester
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2021
• 资助国家: 英国
• 起止时间: 2021 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FT026995%2F1
• 关键词: EnnCore; End; Conceptual; Guarding; Neural

EnnCore will address a fundamental security problem in neural-based (NB) architectures, allowing system designers to specify and verify a conceptual/behavioral hardcore to the system, which can be used to safeguard NB systems against unanticipated behavior and attacks. It will pioneer the dialogue between contemporary explainable neural models and full-stack neural software verification. We will, therefore, develop methods, algorithms and tools to achieve fully-verifiable intelligent systems, which are explainable, whose correct behavior is guaranteed, and that are robust towards attacks.EnnCore will be validated on three diverse and high-impact application scenarios: (i) securing an AI system for cancer diagnosis (health -- Cancer Research UK, The Christie); (ii) ensuring ethical and legal behavior of a conversational agent (health -- Cancer Research UK, The Christie); and (iii) securing an AI system for demand response (energy -- Urbanchain). The use cases will be co-designed and validated under real-world data conditions with the help of one clinical and one industrial partner.As a result, EnnCore will address a fundamental research problem to ensure the security of neural-enabled components by taking into account its entire lifecycle from development to deployment. Solving this research problem will have a far-reaching impact on areas such as health care, ethically grounded AI and demand response, which heavily depend on secure and trusted software components to meet safety-critical requirements. Therefore, our overall research objective is to have a long-term impact on writing secure and trusted AI-based software components, thus contributing to a shared vision of fully-verifiable software, where underlying NB-based architectures are built with strong symbolic and mathematical guarantees.To achieve this objective, EnnCore will design and validate a full-stack symbolic safeguarding system for NB architectures. This project will advance the state-of-the-art in the development of secure Deep Neural Network (DNN) models by mapping, using and extending explainability properties of existing neuro-symbolic DNN architectures (e.g., Graph Networks, Differentiable Inductive Logic Programming), thus safeguarding them with symbolic verification, abstract interpretation and program synthesis methods. EnnCore will pioneer the multi-disciplinary dialogue between explainable DNNs and formal verification.In particular, EnnCore will deliver safeguarding for safety-critical NB architectures with the following novel properties:(1) Full-stack symbolic software verification: we will develop the first bit-precise and scalable symbolic verification framework to reason over actual implementations of DNNs, thereby providing further guarantees of security properties concerning the underlying hardware and software, which are routinely ignored in existing literature.(2) Explainability / Interpretability: EnnCore will pioneer the integration of knowledge-based and neural explainability methods to support end-users specifying security constraints and diagnosing security risks, in order to provide assurances about its security as NB models evolve. Particular attention will be given to the quantitative and qualitative characterization of semantic-drift phenomena in security scenarios. (3) Scalable: we will systematically combine contemporary symbolic methods for explaining, interpreting and verifying neural representations. In particular, we will develop a neuro-symbolic safeguard framework by linking the structural knowledge-based representation elements to the attentional architecture elements, to achieve scalability and precision in an unprecedented manner. We will also develop new learning techniques for reusing information across different verification runs to reduce formulae size and consistently to improve constraint solving.

encore将解决基于神经系统（NB）架构的基本安全问题，允许系统设计人员指定和验证系统的概念/行为核心，可用于保护NB系统免受意外行为和攻击。它将开创当代可解释神经模型和全栈神经软件验证之间的对话。因此，我们将开发方法、算法和工具来实现完全可验证的智能系统，这些系统是可解释的，其正确行为得到保证，并且对攻击具有鲁棒性。encore将在三个不同的高影响力应用场景中进行验证：(i)确保用于癌症诊断的人工智能系统（健康-英国癌症研究中心，佳士得）；（ii）确保对话代理的道德和法律行为（健康——英国癌症研究中心，佳士得）；（iii）确保需求响应的人工智能系统（能源—Urbanchain）。在一个临床和一个工业合作伙伴的帮助下，用例将在现实数据条件下共同设计和验证。因此，encore将解决一个基础研究问题，通过考虑神经驱动组件从开发到部署的整个生命周期，确保其安全性。解决这一研究问题将对医疗保健、基于道德的人工智能和需求响应等领域产生深远影响，这些领域严重依赖于安全可靠的软件组件来满足安全关键要求。因此，我们的总体研究目标是对编写安全和可信的基于人工智能的软件组件产生长期影响，从而有助于实现完全可验证软件的共享愿景，其中基于nb的底层架构是用强大的符号和数学保证构建的。为了实现这一目标，encore将为NB架构设计并验证一个全栈符号保护系统。该项目将通过映射，使用和扩展现有神经符号DNN架构（例如，图网络，可微分归纳逻辑规划）的可解释性属性，从而通过符号验证，抽象解释和程序合成方法来保护它们，从而推进安全深度神经网络（DNN）模型开发的最新技术。encore将引领可解释深度神经网络与正式验证之间的多学科对话。特别是，encore将为具有以下新特性的安全关键NB架构提供保障：(1)全栈符号软件验证：我们将开发第一个位精确和可扩展的符号验证框架，以对dnn的实际实现进行推理，从而提供有关底层硬件和软件的安全属性的进一步保证，这在现有文献中通常被忽略。(2)可解释性/可解释性：ncore将率先集成基于知识和神经的可解释性方法，以支持最终用户指定安全约束和诊断安全风险，从而在NB模型发展的同时为其安全性提供保证。将特别注意安全情景中语义漂移现象的定量和定性特征。(3)可扩展性：我们将系统地结合当代符号方法来解释、解释和验证神经表征。特别是，我们将通过将结构化的基于知识的表示元素与注意架构元素联系起来，开发一个神经符号保护框架，以前所未有的方式实现可扩展性和精度。我们还将开发新的学习技术，以便在不同的验证运行中重用信息，以减少公式大小并始终改进约束求解。

项目成果

Single Event Effects Assessment of UltraScale+ MPSoC Systems Under Atmospheric Radiation

大气辐射下 UltraScale MPSoC 系统的单粒子效应评估

• DOI: 10.1109/tr.2023.3312548
• 发表时间: 2023
• 期刊: IEEE Transactions on Reliability
• 影响因子: 5.9
• 作者: Agiakatsikas D

Bridging the Gap Between AI and Reality - First International Conference, AISoLA 2023, Crete, Greece, October 23-28, 2023, Proceedings

弥合人工智能与现实之间的差距 - 第一届国际会议，AISoLA 2023，希腊克里特岛，2023 年 10 月 23-28 日，会议记录

• DOI: 10.1007/978-3-031-46002-9_4
• 发表时间: 2024
• 作者: Bensalem S

Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs

• DOI: 10.1109/access.2022.3223359
• 发表时间: 2022-06
• 期刊: IEEE Access
• 影响因子: 3.9
• 作者: Fatimah Aljaafari;R. Menezes;Edoardo Manino;F. Shmarov;Mustafa M. Mustafa-Mustafa-M.-Mustafa-2170073934;L. Cordeiro

Bridging formal methods and machine learning with model checking and global optimisation

• DOI: 10.1016/j.jlamp.2023.100941
• 发表时间: 2024-02
• 期刊: J. Log. Algebraic Methods Program.
• 作者: S. Bensalem;Xiaowei Huang;Wenjie Ruan;Qiyi Tang;Changshun Wu;Xingyu Zhao

Weight-based Semantic Testing Approach for Deep Neural Networks

• 发表时间: 2023
• 作者: Amany Alshareef;Nicolas Berthier;Sven Schewe;Xiaowei Huang