Fall Days on System and Software Analysis

Villa Vennendal, Nunspeet, (see Google maps)
November 6-10, 2017

The IPA Fall Days are an annual multi-day event, dedicated to a specific theme of current interest to the research community of IPA. This year’s Fall Days are dedicated to System and Software Analysis, fitting in the Cyber Physical Systems, Software Analysis and Model-Driven Software Engineering focus areas of the research school for the period 2013-2018.

The programme of the Fall Days will be composed with the help of Jurriaan Hage (UU/e),  Alfons Laarman (UL) and Erik de Vink (TU/e and CWI). Drop us an email if you are interested in giving a presentation during the Fall Days and we’ll see how and where it can fit.

Programme

Monday 6 November is reserved for the IPA PhD workshop; the remainder of the days are devoted to various themes and topics in System and Software Analysis. Our keynote speaker for the PhD Workshop is Sung-Shik Jongmans, winner of the IPA Dissertation Award of 2016.

The PhD workshop aims to promote the interaction and cohesion with PhD students from other universities on both a social and technical level, provide a hospitable setting in which presentation skills can be demonstrated and improved through constructive feedback by peers, and be fun. This workshop is open to all IPA PhD students alike (provided we have sufficient number of time slots). If you are interested in giving a 20-25 minute presentation, send us an email.

Registration

Registration closes on 27 October. Follow this link to register. As always, IPA PhD students can attend for free. For others, details on pricing will be made available upon request.

To make maximal use of the available capacity, we process applications on the following basis: Registrations are treated “first come, first served”. In principle, all PhD students (IPA and non-IPA) will share a room. Others may also be asked to share if we run out of rooms. Until the registration deadline, we will accept participants until we run out of space at the hotel!

A tentative programme is available below.

MONDAY 6 NOVEMBER: PHD WORKSHOP

11:30-12:00 Registration
12:00-13:10 Lunch
13:30-13:35 Opening PhD Workshop
13:35-14:05 Sangeeth Kochanthara, TU/e
Monitor Synthesis for Automotive systems
TBA
14:05-14:35 Petra van den Bos, RU
The Holy Grail of Model-Based Testing: a Complete Test Suite
Model-based testing is a technique for automatically deriving test cases from a model that describes the behaviour of a system. A big challenge in applying this technique is test selection: deriving as few as possible test cases that uncover as many bugs as possible in the system. In my presentation, I will explain how to find a complete test suite, i.e. a set of test cases that can detect any fault, for systems smaller than a predetermined size.
14:35-15:00 Coffee break
15:00-15:30 TBA
TBA
TBA
15:30-16:00 TBA
TBA
TBA
16:00-16:30 Coffee break
16:30-16:35 Award Ceremony
16:30-17:30 Sung-Shik Jongmans, OU
TBA
TBA
17:30-18:30 Drinks
18:30- Dinner

TUESDAY 7 NOVEMBER

9:00-9:45 Bart Jacobs, KU Leuven
Separation logic-based symbolic execution for verification and analysis of pointer-manipulating programs
I introduce separation logic, a successful extension of Hoare logic for reasoning about single-threaded and multithreaded programs involving pointers and other forms of aliasing.
I explain how separation logic has been used successfully for effective symbolic execution of programs and program modules, both for modular formal verification and for whole-program analysis.
9:45-10:30 Dan Zhang, TU/e
TBA
TBA
10:30-11:00 Coffee
11:00-12:00 Marieke Huisman, UT
Verification of Deterministic Parallel Programs
The use of separation logic has greatly advanced the verification of concurrent software. Much of this work focuses on verification of heterogeneous threads, as used e.g. in Java. In this presentation, I show how separation logic also can be used to reason about programs using homogeneous threading, i.e., where all threads execute the same instructions. Concretely, I discuss how separation logic is used to verify OpenCL kernels (for GPU architectures), as well as OpenMP compiler directives for parallelisation. All verifications are supported in the VerCors tool set for verification of concurrent software.
12:15-13:30 Lunch
14:00-15:00 Roberto Giacobazzi, University of Verona
Securing Code — Hacking the precision of program analysis
The talk concerns the design of code protecting transformations for anti reverse engineering applications. These technologies are widely used in code protection (e.g., IP protection or key protection), malware design, anti tampering, code watermarking and birth-marking of code. The battle scenario involves attackers intended to extract information by reverse engineering the code, and protecting code transformations modeled as distorted compilers devoted to inhibit these attacks. Attacks are inhibited by maximizing imprecision in all attempts made by the attacker to exploit control and data-flow of the obscured code. After a brief survey on the state of the art in the field, we introduce a model for code obfuscation which is general enough to include generic automated static and dynamic attacks. Protecting transformations are then systematically and formally derived as distorted compilers, obtained by specializing a suitably distorted interpreter for the given programming language with respect to the source code to protect. Interestingly this distortion corresponds precisely to defeat the potency of the expected attacker, which is itself an interpreter and whose potency consists in its ability to extract a complete and precise view of program’s execution.
15:00-15:30 Coffee
15:30-16:15 Frits Vaandrager, RU
Learning Mealy Machines with Timers
(joint work with Bengt Jonsson)

Active automata learning is emerging as a highly effective bug finding technique, with applications in areas such as banking cards, network protocols and legacy software. Timing often plays a crucial role in these applications, but cannot be handled adequately by existing algorithms. Even though there has been significant progress on algorithms for active learning of timed models, these approaches are not yet practical due to limited expressivity and/or high complexity.

In order to address this problem, we introduce a simple model of Mealy machines with timers that is able to model the timing behavior of a large class of practical systems, and present a new and efficient algorithm for active learning of this type of automata.

16:15-17:00 Wil Michiels, NXP and TU/e
TBA
TBA
18:00-20:00 Dinner

WEDNESDAY 8 NOVEMBER

09:00-10:00 Frank Takes, UL
TBA
TBA
10:00-10:30 Coffee
10:30-11:15 Jan Martijn van der Werf, UU
TBA
TBA
11:15-12:00 Bram Cappers, TU/e
Network Traffic Analysis using Deep Packet Inspection and Data Visualization
Many domains nowadays try to gain insight in complex systems by logging their behavior. Telecom companies for instance analyze their communication networks for the presence of fraud, hospitals analyze patient treatments to discover bottlenecks in the process, and companies study their work flows to improve customer satisfaction. The common ground here is that these domains are interested in the analysis of events.

In this presentation we will discuss the role of data visualization for the detection and explanation of anomalous patterns in event data. In particular, we will show how these visualization techniques can be used for the protection of critical infrastructures against complex virus attacks (a.k.a. Advanced Persistent Threats). In our project SpySpot, we will demonstrate the effectiveness of the system on real-world traffic including VoIP communication and Ransomware activity in file systems.

12:15-13:30 Lunch
14:00-15:00 Joost Visser, RU and SIG
TBA
TBA
15:00-15:30 Coffee
15:30-16:15 Alexander Serebrenik, TU/e
TBA
TBA
16:15-17:00 TBA
TBA
TBA
18:00-20:00 Dinner

THURSDAY 9 NOVEMBER

09:00-10:00 Jurgen Vinju, CWI
Analyzing Java and C++ source code using Rascal
This is a short introduction into the Rascal metaprogramming language and its libraries for analyzing Java and C++ source code. This “lab” infra-structure is used in a wide variety of academic and industrial projects, ranging from metric suites to static analyses and large scale empirical (field) studies on open-source projects. In this talk we introduce the language and these two libraries and take your through a small number of examples. We discuss the quality of the resulting analyses in terms of accuracy (false positive and false negative rates).
10:00-10:30 Coffee
10:30-11:15 Jurriaan Hage, UU
TBA
TBA
11:15-12:00 Markus Klinik, RU
Predicting Resource Consumption of Higher-Order Workflows
We present a type and effect system for the static analysis of programs written in a simplified version of iTasks.
iTasks is a workflow specification language embedded in Clean, a general-purpose functional programming language.
Given costs for basic tasks, our analysis calculates an upper bound of the total cost of a workflow.
The analysis has to deal with the domain-specific features of iTasks, in particular parallel and sequential composition of tasks, as well as the general-purpose features of Clean, in particular let-polymorphism, higher-order functions, recursion and lazy evaluation.
Costs are vectors of natural numbers where every element represents some resource, either consumable or reusable.
12:15-13:30 Lunch
14:00-15:00 John Hughes, Chalmers University of Technology, Sweden and Quviq AB
TBA
TBA
15:00-15:30 Coffee
15:30-16:15 Jan Tretmans, RU and TNO-ESI
TBA
TBA
16:15-17:00 Marcus Gerhold, UT
TBA
TBA
18:00-20:00 Dinner
20:45- Social Event

FRIDAY 10 NOVEMBER

09:30-10:30 Arend Rensink, UT
Abstract graph transformation for pointer analysis
TBA
10:30-11:00 Coffee
11:00-11:45 TBA
TBA
TBA
11:45-12:30 TBA
TBA
TBA
12:30-13:30 Lunch