COOL-MC: A Comprehensive Tool for Learning and Model Checking

Deep Reinforcement Learning (RL) is a state-of-the-art technique to synthesize sequential decision-making policies.
However, these synthesized policies lack guarantees and limit the applications of deep RL in safety-critical scenarios.
Probabilistic model checking can verify these policies, but no tool support RL and model checking.
This tool support is needed to foster further integration of RL and model checking.
COOL-MC makes it straightforward to synthesize and verify policies by extending the OpenAI gym with a probabilistic model checking interface.

Authors: Dennis Gross, Nils Jansen, Sebastian Junges, and Guillermo A. Pérez

Workshop Presentation: RL-CONFORM_IROS 2021


Published: SETTA 2022: Symposium on Dependable Software Engineering: Theories, Tools and Applications


Robustness Verification for Classifier Ensembles

We give a formal verification procedure that decides whether a classifier ensemble is robust against arbitrary randomized attacks. Such attacks consist of a set of deterministic attacks and a distribution over this set. The robustness-checking problem consists of assessing, given a set of classifiers and a labelled data set, whether there exists a randomized attack that induces a certain expected loss against all classifiers. We show the NP-hardness of the problem and provide an upper bound on the number of attacks that is sufficient to form an optimal randomized attack. These results provide an effective way to reason about the robustness of a classifier ensemble. We provide SMT and MILP encodings to compute optimal randomized attacks or prove that there is no attack inducing a certain expected loss. In the latter case, the classifier ensemble is provably robust. Our prototype implementation verifies multiple neural-network ensembles trained for image-classification tasks. The experimental results using the MILP encoding are promising both in terms of scalability and the general applicability of our verification procedure.

Authors: Dennis Gross, Nils Jansen, Guillermo A. Pérez, Stephan Raaijmakers


Published: ATVA 2020 The 18ᵗʰ International Symposium on Automated Technology for Verification and Analysis

Adversarial Patch Camouflage against Aerial Detection

Detection of military assets on the ground can be performed by applying deep learning-based object detectors on drone surveillance footage. The traditional way of hiding military assets from sight is camouflage, for example by using camouflage nets. However, large assets like planes or vessels are difficult to conceal by means of traditional camouflage nets. An alternative type of camouflage is the direct misleading of automatic object detectors. Recently, it has been observed that small adversarial changes applied to images of the object can produce erroneous output by deep learning-based detectors. In particular, adversarial attacks have been successfully demonstrated to prohibit person detections in images, requiring a patch with a specific pattern held up in front of the person, thereby essentially camouflaging the person for the detector. Research into this type of patch attacks is still limited and several questions related to the optimal patch configuration remain open.
This work makes two contributions. First, we apply patch-based adversarial attacks for the use case of unmanned aerial surveillance, where the patch is laid on top of large military assets, camouflaging them from automatic detectors running over the imagery. The patch can prevent automatic detection of the whole object while only covering a small part of it. Second, we perform several experiments with different patch configurations, varying their size, position, number and saliency. Our results show that adversarial patch attacks form a realistic alternative to traditional camouflage activities, and should therefore be considered in the automated analysis of aerial surveillance imagery.

Authors: Ajaya Adhikari, Richard den Hollander, Ioannis Tolios, Michael van Bekkum, Anneloes Bal, Stijn Hendriks, Maarten Kruithof, Dennis Gross, Nils Jansen, Guillermo Pérez, Kit Buurman, Stephan Raaijmakers


Published: SPIE Security + Defence 2020 Digital Forum 21

In the news:

An Introduction to Secure Machine Learning

Machine Learning has created a seismic shift in how we think about software engineering and building things in general. Instead of asking how we should solve things ourselves, we dream of being able to just point at the data and let probabilistic systems make an objectively accurate decision for us.

Lately, there has been a growing conversation about the various risks inherent in these sorts of models and how we should be mitigating against them. The field of secure machine learning attempts to address this problem. The idea in its most basic form is to act proactively by putting yourself in the mindset of a criminal and ‘hacking’ into your own machine learning systems to identify problems, weak spots, or potential back doors before an actual criminal can do the same.  After reading this book, you will understand the fundamentals and how you can dive deeper into the field of secure machine learning.