Neural networks have been successfully adopted in many security-critical systems. Neural network verification is gaining more interest, since these models can be attacked and fooled in several different ways. In this paper, we propose a formal approach to verify some security properties of neural networks. The overall approach goes through three steps: (1) specify security objectives as properties of a modeled neural network in a technology-independent specification language; (2) implement the developed model in a suitable tooled language for analysis; and (3) suggest a set of security requirements necessary to fulfill the targeted security objectives. We use first-order logic and modal logic as abstract and technology independent formalism and Alloy as a tooled language. To validate our work, we explore a set of representative security objectives from the Confidentiality, Integrity, and Availability classification in a use case from the unmanned aircraft domain.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Formal Security Analysis of Deep Neural Network Architecture

  • Marwa Zeroual,
  • Brahim Hamid,
  • Morayo Adedjouma,
  • Jason Jaskolka

摘要

Neural networks have been successfully adopted in many security-critical systems. Neural network verification is gaining more interest, since these models can be attacked and fooled in several different ways. In this paper, we propose a formal approach to verify some security properties of neural networks. The overall approach goes through three steps: (1) specify security objectives as properties of a modeled neural network in a technology-independent specification language; (2) implement the developed model in a suitable tooled language for analysis; and (3) suggest a set of security requirements necessary to fulfill the targeted security objectives. We use first-order logic and modal logic as abstract and technology independent formalism and Alloy as a tooled language. To validate our work, we explore a set of representative security objectives from the Confidentiality, Integrity, and Availability classification in a use case from the unmanned aircraft domain.