Towards logical specification of adversarial examples in machine learning
Résumé
The use of Artificial Intelligence (AI)-based systems, using particularly Machine Learning (ML) classifiers, is growing rapidly and finding uses in many industries. Most of these industries have critical safety, security, and dependability requirements. Despite this rapid growth, interest in the security of these systems has only arisen in the last few years and it is not yet well-studied. There is a want for a formal notion of security for ML systems, similar to that used in classical information security. We took this statement toward security threat modeling and analysis in ML-based systems, focusing on the adversarial example threat.
An adversarial example threat is an input of the classifier that was maliciously modified to induce a misclassification. Identifying this threat at the architecture design stage before proceeding with system development is a critical milestone in the development process of secure ML systems. In this paper, we propose an approach to adversarial example threat specification and detection in component-based software architecture models. We use first-order and modal logic as an abstract and technology-independent formalism.
The general idea of the approach is to specify the threat as property of a modeled system such that the violation of the specified property indicates the presence of the threat. We demonstrate the applicability of the method through a classifier used in a recommendation system.