The workshop addressed the theme of formal method for the design of critical systems. Our guests, who were in Trento for the Ph.D. dissertation of Sergio Mover, presented a number of studies conducted in this area. The program included an approach for detecting sensor spoofing attacks on a cyber-physical system, one for the verification of hybrid systems with the open-source framework Ariadne, the use of unfoldings in automated testing of multithreaded programs, and an overview of SATMC 3.0, which is a SAT-based bounded model checker for security-critical systems.
The Workshop was held at Fondazione Bruno Kessler (FBK) in Trento, Italy, March 19th, 2014 (Sala Conferenze “Luigi Stringa”).
Address:
Fondazione Bruno Kessler (FBK)
Center for scientific and Technological Reasearch
Via Sommarive, 18
I-38123 Trento, Italy
tel.(+39) 0461 314 444
General Info
- Start: 19 Mar 2014 13:30
- End: 19 Mar 2014 17:00
- Location: Sala Conferenze “Luigi Stringa”
Programme
The program will consist of:
- Four Invited talks, by:
- Ashish Tiwari (SRI International), and
- Tiziano Villa (University of Verona),
- Keijo Helianko (Aalto University),
- Alessandro Armando(University of Genova and FBK);
A substantial amount of the program was reserved for discussion, feedback and interaction among participants.
Wednesday, March 19, 2014
| Session1 | |
| 13.30-14.15 | Ashish Tiwari (SRI International) Safety Envelope for Security Slides |
| 14.15-15.00 | Tiziano Villa (University of Verona) An introduction to the verification of hybrid systems using Ariadne Slides |
| 15.00-15.30 Break | |
| Session2 | |
| 15.30-16.15 | Keijo Helianko (Aalto University) Using unfoldings in automated testing of multithreaded programs Slides Slides |
| 16.15-17.00 | Alessandro Armando (University of Genova and FBK) SATMC: a SAT-based Model Checker for Security-critical Systems Slides Slides |
Program Details
13.30 - 14.15
Speaker: Ashish Tiwari (SRI International)
Title: Safety Envelope for Security
Abstract: We present an approach for detecting sensor spoofing attacks on a cyber-physical system. Our approach consists of two steps.
In the first step, we construct a safety envelope of the system. Under nominal conditions (that is, when there are no attacks), the system always stays inside its safety envelope.
In the second step, we build an attack detector monitor that executes synchronously with the system and raises an alarm whenever the system state falls outside the safety envelope.
We synthesize safety envelopes using a modifed machine learning procedure applied on data collected from the system when it is not under attack. We present experimental results that show effectiveness of our approach, and also validate the several novel features that we introduced in our learning procedure.
14.15 - 15.00
Speaker: Tiziano Villa (University of Verona) (joint work with Davide Bresolin, Luca Geretti and Pieter Collins)
Title: An introduction to the verification of hybrid systems using Ariadne
Abstract: We introduce the verification of hybrid systems as offered by the open-source framework called Ariadne, which is a C++ library that applies approximation techniques for implementing formal verification algorithms based on reachability analysis. Ariadne relies on the theory of computable analysis to guarantee rigorous approximations. We demonstrate the tool using a classical example of a controlled water tank system.
15.30 - 16.15
Speaker: Keijo Helianko (Aalto University)
Title: Using unfoldings in automated testing of multithreaded programs
Abstract: In multithreaded programs both environment input data and the nondeterministic interleavings of concurrent events can affect the behavior of the program. One approach to systematically explore the nondeterminism caused by input data is dynamic symbolic execution. For testing multithreaded programs we present a new approach that combines dynamic symbolic execution with unfoldings, a method originally developed for Petri nets but also applied to many other models of concurrency.
We provide an experimental comparison of our new approach with existing algorithms combining dynamic symbolic execution and partial-order reductions and show that the new algorithm can explore the reachable control states of each thread with a significantly smaller number of test runs. In some cases the reduction to the number of test runs can be even exponential allowing programs with long test executions or hard-to-solve constrains generated by symbolic execution to be tested more efficiently.
16.15 - 17.00
Speaker: Alessandro Armando (University of Genova and FBK) (joint work with Roberto Carbone e Luca Compagna)
Title: SATMC: a SAT-based Model Checker for Security-critical Systems
Abstract: We present SATMC 3.0, a SAT-based bounded model checker for security-critical systems that stems from a successful combination of encoding techniques originally developed for planning with techniques developed for the analysis of reactive systems. SATMC has been successfully applied in variety of application domains (security protocols, security-sensitive business processes, and cryptographic APIs) and for different purposes (design-time security analysis and security testing).
SATMC strikes a balance between general purpose model checkers and security protocol analyzers as witnessed by a number of important success stories including the discovery of a serious man-in-the-middle attack on the SAML-based Single Sign-On (SSO) for Google Apps, an authentication flaw in the SAML 2.0 Web Browser SSO Profile, and a number of attacks on PKCS#11 Security Tokens. SATMC is integrated and used as back-end in a number of research prototypes (e.g. the AVISPA Tool, Tookan, the SPaCIoS Tool) and industrial-strength tools (e.g. the Security Validator plugin for SAP NetWeaver BPM).