Formal Security Analysis of Deep Neural Network Architecture

Formal Security Analysis of Deep Neural Network Architecture

연구 분야: Networking

학회: International Conference on Verification and Evaluation of Computer and Communication Systems

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.