Workshop and Working Groups Meeting
Sept 3 Workshop – from 9:00 to 17:30
Sept 4 Working Groups Meeeting – from 9:00 to 17:30
The meeting will be held in Siracusa (Sicily island) at the Siracusa Impact Hub in the hearth of the Ortigia island (exact address Via Mirabella 29 – 96100 Siracusa|Ortigia).
There are many places that you can find searching online on Booking and Airbnb. If possible, we recommend you to stay within the Ortigia island since it is the old part of the city.
You can find below a few places you might consider both inside and outside the Ortigia island:
Walking distance from the meeting place:
- Hotel Livingston (about 120 EUR per night) – 7 minutes walking distance http://www.booking.com/Share-NXC1Gq
- Antico Hotel Roma (about 90 EUR per night) – 5 minutes walking distance http://www.booking.com/Share-mR5YIn
- Grande Albergo Alfeo (about 100 EUR per night) – 10 minutes walking distance http://www.booking.com/Share-CLVWMC
- UNA Hotel One Spa & Wellness (about 90 EUR per night) – 17 minutes by taxi http://www.booking.com/Share-yy8hud
- Hotel Parco delle Fontane (about 100 EUR per night) – 20 minutes by taxi http://www.booking.com/Share-wZZIaz
- Grand Hotel Villa Politi (about 75 per night) – 15 minutes by taxi http://www.booking.com/Share-CViu76
To get to Siracusa, the closest airport is in Catania Iternational Airport (www.aeroporto.catania.it/?lang=en). From the airport, you can get to Siracusa either:
• By bus: INTERBUS (www.interbus.it) runs hourly buses (8:40am–8:40pm) between the Catania airport and Siracusa (at Corso Umberto 196). The cost will range between EUR 6 and EUR 7. From the stop in Siracusa, you may need to take a Taxi to get to your hotel.
• By taxi: Radio Taxi Siracusa (e.g., www.radiotaxisiracusa1844.net) – you have to reserve the taxi in advance. The cost will range between EUR 50 and EUR 60.
• By car: Siracusa is 64km (45 miles) south of the Catania airport. From the Catania airport, take the SP701 out to the A18 autostrada and just follow that south to Siracusa. 1 hr.
Ryanair has some flights to Comiso Airport (Airport “Pio La Torre”, Comiso RG). This is a smaller airport and somehow less organised as services. In fact, some bus transfers can be indirect, meaning that they may require you to get off at an intermediate stop and change bus. From Comiso, get to Siracusa either:
• By bus: The cost will range between EUR 4 and EUR 6. From the stop in Siracusa, you may need to take a Taxi to get to your hotel.
• By taxi: The cost will range between EUR 110 and EUR 140.
• By car: Siracusa is about 87 Km north from Comiso.
You can find useful information about Siracusa here.
You can find many restaurants in the whole Ortigia, in particular along the streets indicated in the map.
Monday, 3 Sept
Workshop on Privacy & Security
08:55 – 9:00 Welcome
9:00 – 10:30 – Session I
Bernd Finkbeiner, Universität des Saarlandes, Germany
Hyperproperties, such as non-interference and observational determinism, relate multiple system executions to each other. They are not expressible in standard temporal logics, like LTL, CTL, and CTL*, and thus cannot be monitored with standard runtime verification techniques. HyperLTL extends linear-time temporal logic (LTL) with explicit quantification over traces in order to express Hyperproperties. We investigate the runtime verification problem of HyperLTL for three different input models: (1) The parallel model, where a fixed number of system executions is processed in parallel. (2) The unbounded sequential model, where system executions are processed sequentially, one execution at a time. In this model, the number of incoming executions may grow forever. (3) The bounded sequential model where the traces are processed sequentially and the number of incoming executions is bounded. We show that deciding monitorability of HyperLTL formulas is PSPACE-complete for input models (1) and (3). Deciding monitorability is PSPACE-complete for alternation-free HyperLTL formulas in input model (2). For every input model, we provide practical monitoring algorithms. We also present various optimization techniques. By recognizing properties of specifications such as reflexivity, symmetry, and transitivity, we reduce the number of comparisons between traces. For the sequential models, we present a technique that minimizes the number of traces that need to be stored. Finally, we provide an optimization that succinctly represents the stored traces by sharing common prefixes. The evaluation of our optimizations shows that this leads to much more scalable monitoring, in particular, significantly lower memory consumption. The talk is based on joint work with Christopher Hahn, Marvin Stenger, and Leander Tentrup.
Runtime Verification of Hyperproperties for Deterministic Programs
Gerardo Schneider, University of Gothenburg, Sweden
In this talk I will present some results concerning the runtime monitoring of safety hyperproperties for deterministic programs. Several security and information-flow policies such as data minimality, non-interference, integrity, and software doping are naturally expressed formally as safety hyperproperties. Although there are monitoring results for hyperproperties, the algorithms are very complex since these are properties over set of traces, and not over single traces. For the deterministic input-output programs that we consider, and the specific safety hyperproperties we are interested in, the problem can be reduced
to monitoring of trace properties. I will present a simpler monitoring approach for safety hyperproperties of deterministic programs. The approach involves transforming the given safety hyperproperty into a trace property, extracting a characteristic predicate for the given hyperproperty, and providing a parametric monitor taking such predicate as parameter. Joint work with Srinivas Pinisetty and Dave Sands
Runtime Verification of Security Properties with E-ACSL
Julien Signoles, CEA LIST, Software Security Labs, France
Frama-C is a framework for code analysis of C code, including many analyzers. This talk presents E-ACSL, the Frama-C’s runtime verification tool, and its applications to verification of security properties. E-ACSL automatically converts a C code annotated with formal specifications to another C code that checks them at runtime. Several usages of E-ACSL rely on automatic generation of these specifications, so that writing them by hand is not necessary. The verification process is therefore fully automatic. In this talk, we will focus on such automatic usages for verification of security properties, including verification of memory safety properties and information flow properties.
10:30 – 11:00 Coffee break
11:00 – 12:30 – Session II
Practical policy enforcement in data-oriented systems
Deepak Garg, Max Planck Institute for Software Systems, Germany
Many services today collect, index, process and serve sensitive user data. It is in the interest of both service providers and users that data, whether that collected directly or derived indirectly, always be used in accordance with applicable privacy polices. However, ensuring bug-free compliance with policies without imposing significant runtime overhead is very difficult in practical, large-scale software systems. To start, most relevant policies are dynamic, meaning that they depend on runtime information, so purely static enforcement is impossible. Other methods like taint-tracking using hardware or software techniques have prohibitively high overhead.
In this talk, I will describe an approach to enforcing dynamic policies end-to-end by relying on coarse-grained runtime
monitoring. The idea comes from coarse-grained information flow control—rather than examine code statically or monitor code
execution at runtime, we only intercept process I/O at runtime. Using this, we approximate data flows coarsely, and then enforce access and declassification policies, end-to-end. This is precise enough for practical data retrieval pipelines, and has only low to moderate overhead. We reduce the runtime overhead even further by using system lean periods to predictively check policies along (coarse-grained) flows that may arise in the future and to compile flows so certified to low-level kernel permissions.
Searching Encrypted Data in the Cloud
Bernardo Ferreira, Universidade Nova de Lisboa, Portugal
Searchable Symmetric Encryption (SSE) has emerged as an important research topic in recent years, allowing one to efficiently query and update an encrypted database within an untrusted server, with privacy and reliability guarantees. SSE has obvious and very beneficial applications for cloud deployments, especially for healthcare, biomedicine, and life science organizations that are adopting cloud platforms but are nonetheless subject to strict governmental regulations regarding data privacy and confidentiality. However achieving a good balance between security, performance, and usability in SSE is no easy task, with existing schemes usually being forced to make a hard tradeoff between these three aspects. In this talk we will discuss the state of the art in SSE and how existing schemes have addressed the security-performance-usability tradeoff. Then we will discuss how we can improve on the literature even further.
Information flow monitoring in an actor-based distributed programming language
Aslan Askarov, Aarhus University, Denmark
This talk presents the design and implementation of a concurrent and distributed programming language with dynamic information flow control. The surface-level language is a subset of Erlang, but the underlying runtime is designed with information flow control in mind. A particular aspect of the system is the intermediate representation that is used by the compiler and that it is amenable to standard information flow monitoring techniques. The talk will include the demo of the current prototype and discussion of the security properties of the system.
12:30 – 14:30 Lunch break
14:30 – 15:30 – Session III
Securing IoT Apps
Andrei Sabelfed, Chalmers University of Technology, Sweden
IoT apps empower users by connecting a variety of otherwise unconnected services. Unfortunately, the power of IoT apps can be abused by malicious makers, unnoticeably to users. We demonstrate that popular IoT app platforms are susceptible to several classes of attacks that violate user privacy, integrity, and availability. We present a large-scale empirical study to estimate the scale of possible threats. We suggest short- and medium-term countermeasures based on fine-grained access control and present long-term countermeasures based on tracking the flow of information in IoT apps. Joint work with Iulia Bastys and Musard Balliu.
Information-flow Control in Database-backed Applications
Musard Balliu, KTH Royal Institute of Technology, Sweden
Securing database-backed applications requires tracking information across the program and the database together, since securing each component in isolation may still result in an overall insecure system. Current research extends language-based techniques with models capturing the database’s behavior. Previous work, however, relies on simplistic database models, which ignore security-relevant features that may leak sensitive information.
We propose a novel security monitor for database-backed applications. Our monitor tracks fine-grained dependencies between variables and database tuples by leveraging database theory concepts like disclosure lattices and query determinacy. It also accounts for a realistic database model that supports security-critical constructs like triggers and dynamic policies. The monitor automatically synthesizes program-level code that replicates the behavior of database features like triggers, thereby tracking information flows inside the database. We also introduce symbolic tuples, an efficient approximation of dependency-tracking over disclosure lattices. We implement our monitor for database-backed SCALA programs and demonstrate its effectiveness on four case studies.
This is joint work with Marco Guarnieri and David Basin from ETH Zurich, and Daniel Schoepe and Andrei Sabelfeld from Chalmers.
15:30 – 16:00 Coffee break
16:00 – 17:00 – Session IV
Key establishment using cardiac signals: Can two ECG sensors generate the same token?
Pedro Peris-Lopez, University Carlos III of Madrid, Spain
We are in the era of the Internet of Things (IoT), where all kinds of devices and sensors are connected to the Internet. There are a wide variety of applications/sectors that can benefit from this technology, but it can turn into a nightmare if security does not play a critical role. This is even more critical, if possible, in particular sectors like the health-care sector, where sensors are in or on a subject’s body, and a cybersecurity attack could have dramatic consequences. In the context of cardiac signals, the vast majority of security solutions are based on Inter-Pulse Intervals, as this information can be gathered by an ECG or PPG sensor. The question that we would like to answer is whether two ECG sensors over the same body and in different positions (e.g., wrist and chest) can generate the same cryptographic key using the IPIs sensed by each device. We show how a run-time monitor is useful for this purpose.
Nuno Antunes, University of Coimbra, Portugal
joint dinner at the Al Patio restaurant (https://www.alpatio.it/)
Via Pompeo Picherali, 10
Tuesday, 4 Sept
Cost Action Meeting
09:00 – 10:30 WG3 and WG4 (parallel work)
10:30 – 11:00 Coffee break
11:00 – 12:30 WG3 and WG4 (parallel work)
12:30 – 14:00 Lunch break
14:00 – 15:30 WG1
15:30 – 16:00 Coffee break
16:00 – 17:30 WG2 (if needed) + COST dissemination activities
This event is organized by
Leonardo Mariani (firstname.lastname@example.org)
- Giovanni Denaro (email@example.com)
members of the Laboratory of Testing and Anaysis (LTA).
For any question and additional information, please contact us via email.