Digital Library[ Search Result ]
Layered Abstraction Technique for Effective Formal Verification of Deep Neural Networks
Jueun Yeon, Seunghyun Chae, Kyungmin Bae
http://doi.org/10.5626/JOK.2022.49.11.958
Deep learning has performed well in many areas. However, deep learning is vulnerable to errors such as adversarial examples. Therefore, much research exists on ensuring the safety and robustness of deep neural networks. Since deep neural networks are large in scale and the activation functions are non-linear, linear approximation methods for such activation functions are proposed and widely used for verification. In this paper, we propose a new technique, called layered abstraction, for non-linear activation functions, such as ReLU and Tanh, and the verification algorithm based on that. We have implemented our method by extending the existing SMT-based methods. The experimental evaluation showed that our tool performs better than an existing tool.
SMT-based Formal Verification Methods of Deep Neural Networks using Structural Properties
http://doi.org/10.5626/JOK.2021.48.9.998
Deep neural networks (DNN) are widely used for software in various fields, such as speech recognition and image classification. However, unexpected errors, such as adversarial examples, may exist in DNNs. DNN formal verification techniques to verify the requirements of DNNs are being widely studied in order to prevent these errors. This paper proposes a methodology that utilizes the structural properties of DNNs to increase the performance of DNN verification. This paper mathematically defines the structural property of DNN, suggests two structural properties of DNN with ReLU as an activation function, and shows that the verification speed of SMT-based DNN verification can be increased using the structural properties.
Lightweight Equivalence Checking of Code Transformation for Code Pointer Integrity
Jaeseo Lee, Tae-Hyoung Choi, Gyuho Lee, Jaegwan Yu, Kyungmin Bae
http://doi.org/10.5626/JOK.2019.46.12.1279
Code transformation is widely used to improve the performance and security of programs, but serious software errors can occur in this process if the generated program is not equivalent to the original program. There are a number of approaches for translation validation that can be used to prove the equivalence of programs, but the high cost of proof checking restricts the applicability of these techniques for large programs. In this paper, we propose a practical approach for checking the correctness of LLVM code transformation. We first prove the correctness of the transformation rules using automated theorem proving before compilation. We then perform a simple code analysis method—as opposed to directly proving the program equivalence— to check whether the transformations rules are correctly applied to the generated code. As the complexity of the proposed code analysis is linear, our technique can be effectively applied to large programs, unlike previous techniques. To prove the effectiveness of the proposed approach, we present a case study on LLVM code transformation for a code pointer integrity instrumentation.
Search
Journal of KIISE
- ISSN : 2383-630X(Print)
- ISSN : 2383-6296(Electronic)
- KCI Accredited Journal
Editorial Office
- Tel. +82-2-588-9240
- Fax. +82-2-521-1352
- E-mail. chwoo@kiise.or.kr