Flavio Ferrarotti

Klaus-Dieter Schewe, Flavio Ferrarotti, Peter Rivière et al.

The verification of liveness conditions is an important aspect of state-based rigorous methods. This article addresses the extension of the logic of Event-B to a powerful logic, in which properties of traces of an Event-B machine can be expressed. However, all formulae of this logic are still interpreted over states of an Event-B machine rather than traces. The logic exploits that for an Event-B machine $M$ a state $S$ determines all traces of $M$ starting in $S$. We identify a fragment called TREBL of this logic, in which all liveness conditions of interest can be expressed, and define a set of sound derivation rules for the fragment. We further show relative completeness of these derivation rules in the sense that for every valid entailment of a formula $φ$ one can find a derivation, provided the machine $M$ is sufficiently refined. The decisive property is that certain variant terms must be definable in the refined machine. We show that such refinements always exist. Throughout the article several examples from the field of security are used to illustrate the theory.

Daniel Dorfmeister, Flavio Ferrarotti, Bernhard Fischer et al.

More and more companies' Intellectual Property (IP) is being integrated into Neural Network (NN) models. This IP has considerable value for companies and, therefore, requires adequate protection. For example, an attacker might replicate a production machines' hardware and subsequently simply copy associated software and NN models onto the cloned hardware. To make copying NN models onto cloned hardware infeasible, we present an approach to bind NN models - and thus also the IP contained within them - to their underlying hardware. For this purpose, we link an NN model's weights, which are crucial for its operation, to unique and unclonable hardware properties by leveraging Physically Unclonable Functions (PUFs). By doing so, sufficient accuracy can only be achieved using the target hardware to restore the original weights, rendering proper execution of the NN model on cloned hardware impossible. We demonstrate that our approach accomplishes the desired degradation of accuracy on various NN models and outline possible future improvements.

Bernhard Fischer, Daniel Dorfmeister, Flavio Ferrarotti et al.

Embedded software used in industrial systems frequently relies on data that ensures the correct and efficient operation of these systems. Thus, companies invest considerable resources in fine-tuning this data, making it their valuable intellectual property (IP). We present a novel protection mechanism for this IP that combines hardware fingerprints with Boolean logic. Unlike usual copy-protection approaches, unauthorised copies of the software still run on cloned devices but suboptimally. According to our security evaluation, only a complex dynamic analysis of the protected software running on the genuine target device can reveal the secret data. This makes the protection offered by our method more difficult to bypass. Notably, our approach does not require additional hardware, relying only on relatively simple updates to the software. We evaluate our protection mechanism by binding the parameters of a PID controller to a microcontroller unit (MCU) by using a physically unclonable function (PUF) based on its SRAM.

Daniel Dorfmeister, Flavio Ferrarotti, Bernhard Fischer et al.

We introduce a novel copy-protection method for industrial control software. With our method, a program executes correctly only on its target hardware and behaves differently on other machines. The hardware-software binding is based on Physically Unclonable Functions (PUFs). We use symbolic execution to guarantee the preservation of safety properties if the software is executed on a different machine, or if there is a problem with the PUF response. Moreover, we show that the protection method is also secure against reverse engineering.