Biblio

SCADA control systems use programmable logic controller to interface with critical machines. SCADA systems are used in critical infrastructures, for instance, to control smart grid, oil pipelines, water distribution and chemical manufacturing plants: an attacker taking control of a SCADA system could cause various damages, both to the infrastructure but also to people (for instance, adding chemical substances into a water distribution systems). In this paper we propose a method to detect attacks targeting SCADA systems. We exploit model checking, in detail we model logs from SCADA systems into a network of timed automata and, through timed temporal logic, we characterize the behaviour of a SCADA system under attack. Experiments performed on a SCADA water distribution system confirmed the effectiveness of the proposed method.

Android operating system is constantly overwhelmed by new sophisticated threats and new zero-day attacks. While aggressive malware, for instance malicious behaviors able to cipher data files or lock the GUI, are not worried to circumvention users by infection (that can try to disinfect the device), there exist malware with the aim to perform malicious actions stealthy, i.e., trying to not manifest their presence to the users. This kind of malware is less recognizable, because users are not aware of their presence. In this paper we propose FormalDroid, a tool able to detect silent malicious beaviours and to localize the malicious payload in Android application. Evaluating real-world malware samples we obtain an accuracy equal to 0.94.