Call for Participation - Software Reliability pre-defence workshop: December 12, Enschede
20-Nov-2019
Dear all,
It is my pleasure to invite you to the workshop themed Software Reliability on the 12th of December at the University of Twente, prior to the defence of my PhD thesis titled "Deductive Techniques for Model-Based Concurrency Verification".
This workshop will feature presentations from various speakers, three of which from outside the Netherlands, covering recent research in formal verification of: blockchain programs, embedded control software, IoT operating systems, and parallel GPU algorithms. A lunch is included as well.
The program is as follows:
- 12:30 - 13:30: Lunch @ Carré 3H, University of Twente
- 13:30 - 14:00: Wolfgang Ahrendt (Chalmers University of Technology, Sweden)
Title: Million $ damage through Blockchain programs - What to do?
Abstract: To be announced.
- 14:00 - 14:30: Paula Herber (University of Munster, Germany)
Title: Automated Formal Verification of Embedded Control Systems
Abstract: About 98% of the computing devices produced worldwide are used in embedded systems. The functionality spans from simple microcontrollers in a fridge to complex systems with millions of lines of code, for example in cars, airplanes, or smart factories. In such systems, failure often has serious consequences, such as huge financial losses or even loss of lives. Thus, the correctness and reliability of embedded systems are of vital importance. To achieve this, a clear understanding of the models and languages that are used in the development process is highly desirable. Formal methods provide a basis to make the development process systematic, well-defined, and automated. However, for many industrially relevant languages and models, such as Matlab/Simulink and SystemC, the semantics is only informally defined. Together with the restricted scalability of formal design and verification techniques, this makes the formal verification of embedded control systems a major challenge. In this talk, I will summarize some of my contributions and current research activities in this field.
- 14:30 - 15:00: Coffee/tea break
- 15:00 - 15:30: Nikolai Kosmatov (CEA, List, Software Reliability Lab, France)
Title: Towards Formal Verification of IoT Operating Systems with Frama-C
Abstract: Connected devices and services, also referred to as the Internet of Things (IoT), have proliferated very quickly in the past years. There are now billions of interconnected devices, and this number is rapidly growing. Some of these devices are in service in security critical domains, and even in domains that are not necessarily critical, privacy issues may arise with devices collecting and transmitting a lot of personal information. Moreover, insufficiently secured devices may become a target for massive distributed denial-of-service attacks. This raises important security challenges. It is natural to expect that formal methods—that have been successfully used for years in highly critical domains—can now help to bring security into the IoT field.
A major security threat for IoT devices is related to the underlying software, and in particular, to the operating systems running the connected device. In this talk, we present recent efforts on formal verification of Contiki, an open-source OS for IoT, using the Frama-C verification platform. Contiki provides basic OS features on an event-based kernel, including a scheduler and a networking stack. Contiki focuses on low-power IPv6 connectivity and typically targets devices with an 8 to 32-bit MCU without Memory Management Unit. This makes such devices a target of choice for attackers.
We describe how formal verification with Frama-C can be applied for verification of IoT operating systems and illustrate it for different critical modules of Contiki, namely the memory allocation module, the AES-CCM cryptographic modules, and the linked list module. We discuss the current achievements and future work perspectives. This talk is based on a joint work with Allan Blanchard, Simon Duquennoy, Frédéric Loulergue, Frédéric Mangano, Alexandre Peyrard, and Shahid Raza.
- 15:30 - 16:00: Mohsen Safari (University of Twente, the Netherlands)
Title: Formal Verification of Parallel Prefix Sum
Abstract: With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. Calculating the prefix sum of an array is one of the examples for which various parallel algorithms have been proposed in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe. In this talk, we show correctness of the most frequently used parallel in-place prefix sum algorithms using deductive program verification based on permission-based separation logic, as supported by VerCors, for an arbitrary array size.
- 16:30 - 18:30: Doctoral defence ceremony Wytse Oortwijn
Participation is free of charge. If you wish to attend the workshop + lunch, please register by sending an email to wytse.oortwijn@inf.ethz.ch by December 2 at the latest. If there are any dietary restrictions please include them in the email as well.
Kind regards,
Wytse Oortwijn