Die Tagung findet im Gebäude 50.34 Raum 301 statt (s.u.).
Am Donnerstag (28.11.) treffen wir uns um 19:00 zu einem gemeinsamen Abendessen im
Hoepfner Burghof
(Reservierung auf Schiffl).
Alle Teilnehmenden sind herzlich willkommen!
Programm
Simon Bischof
Probabilistische Nichtinterferenz mit dem RLSOD-Kriterium
Bei parallelen Programmen können geheime Daten bereits durch unterschiedliche
Wahrscheinlichkeiten der öffentlichen Ausgaben geleakt werden. Das sogenannte
LSOD-Kriterium kann solche Lecks erkennen, ist allerdings unpräzise. In diesem
Vortrag werde ich das an unserem Lehrstuhl entwickelte präzisere RLSOD-Kriterium
vorstellen. Zudem werde ich einen kurzen Überblick über den Korrektheitsbeweis
und den Stand der Formalisierung im Theorembeweiser Isabelle geben."
Tim Günesyu
Sicherheit im Zeitalter großskaliger Angreifer - Ein
Überblick zum Exzellenzcluster CASA und dem MPI für
Cybersicherheit in Bochum (Invited Talk)
Dieter Hutter
IT-Sicherheit in Häfen: Das Projekt SecProPort (Short)
Markus Iser
A Problem Meta-Data Library for Research in SAT (Short)
Experimental data and benchmarks play a crucial role in developing new
algorithms and implementations of SAT solvers. Besides comparing and evaluating
solvers, they provide the basis for all kinds of experiments, for setting up
hypothesis and for testing them. Currently – even though some initiatives for
setting up benchmark databases have been undertaken, and the SAT Competitions
provide a “standardized” collection of instances – it is hard to assemble
benchmark sets with prescribed properties. Moreover, the origin of SAT instances
is often not clear, and benchmark collections might contain duplicates. In this
paper we suggest an approach to store meta-data information about SAT instances,
and present an implementation that is capable of collecting, assessing and
distributing benchmark meta-data.
Michael Kirsten
Program-level Noninterference Verification of the Credential Generation in the GI Election Software (Short)
Electronic voting (e-voting) systems used in public elections need to
fulfill strong requirements concerning both safety and security, such as,
e.g., reliability, robustness, privacy of votes, coercion resistance, and
various versions of voter verifiability. Currently, the GI premiers to
perform their annual elections using an e-voting system that provides
a cryptographic eligibility verifiability mechanism. As a core requirement
for this mechanism, the employed voter credentials are not allowed to leak
to the e-voting provider, possibly compromising the eligibility
verifiability. This case study employs the deductive information-flow
calculus of the KeY theorem prover, providing a precise proof that the
source code of the employed credential generation component cannot leak the
voter credentials to untrusted parties. In this talk, I report on our
experiences and the current state of the case study, verifying a non-trivial
security property for a small real-world program of a rich fragment of Java.
Marko Kleine Büning
Automatic Modularization of Large Programs for Bounded Model Checking
The verification of real-world applications is a continuous challenge which
yielded numerous different methods and approaches. However, scalability of
precise analysis methods on large programs is still limited. We thus propose
a formal definition of modules that allows a partitioning of the program
into smaller code fragments suitable for verification by bounded model
checking. We consider programs written in C/C++ and use LLVM as an
intermediate representation. A formal trace semantics for LLVM program runs
is defined that also takes modularization into account. Using different
abstractions and a selection of fragments of a program for each module, we
describe four different modularization approaches. We de ne desirable
properties of modularizations, and show how a bounded model checking
approach can be adapted for modularization. Two modularization approaches
are implemented within the tool QPR-Verify, which is based on the bounded
model checker LLBMC. We evaluated our approach on a medium-sized embedded
system software encompassing approximately 160KLoC.
Andreas Nonnengart
CriSGen: Constraint based Generation of Critical Scenarios for Autonomous Vehicles (Short)
Ensuring pedestrian-safety is paramount to the acceptance and success of
autonomous cars.
The scenario-based training and testing of such self-driving vehicles in
virtual driving simulation environments has increasingly gained
attention in the past years. A key challenge is the automated generation
of critical traffic scenarios which usually are rare in real-world
traffic, while computing and testing all possible scenarios is
infeasible in practice. In this talk, we present a formal method-based
approach, CriSGen, for an automated and complete generation of critical
traffic scenarios for virtual training of self-driving cars. These
scenarios are determined as close variants of given but uncritical and
formally abstracted scenarios via reasoning on their non-linear
arithmetic constraint formulas, such that the original maneuver of the
self-driving car in them will not be pedestrian-safe anymore, enforcing
it to further adapt the behavior during training.
Rhea Rinaldo
Integration of Safety- and Security Reasoning in Automotive Systems
Safety has always been a prior concern in automotive development, but with
the growing connectivity requirements due to the increasing demand for
autonomous features, security concerns are rising dramatically. Safety and
security are partly intertwined, as security incidents can affect the
system's safety and the other way round. Consequently, evaluating both
properties separately is illusive in general, yet still widely adapted in
automotive development. In this talk we address the described problem by
introducing an approach for the integrated safety and security reasoning.
Thereby we abstract the system from details and focus on the interleaving
effects of safety and security, measured by probabilities. On this basis we
define a transformation into a Discrete-Time Markov Chain (DTMC), which
allows for the application of probabilistic model checkers. We describe the
analysis of the system by means of an example and show how possible
weaknesses in the communication structure or due to data dependencies can be
found. \end{talk}
Jonas Schiffl
Smart Contracts: Applications for Deductive Program Verification (Short)
Smart contracts are programs that run on a distributed ledger platform. They
usually manage resources representing valuable assets. Moreover, their
source code is visible to potential attackers, they are distributed, and
bugs are hard to fix. Thus, they are susceptible to attacks exploiting
programming errors. Their vulnerability makes a rigorous formal analysis of
the functional correctness of smart contracts highly desirable.
We show that the architecture of smart contract platforms offers
a computation model for smart contracts that yields itself naturally to
deductive program verification. We discuss different classes of correctness
properties of distributed ledger applications, and show that
design-by-contract verification tools, e.g., the KeY tool, are suitable to
prove these properties.
Guido Schmitz
WIM: An Expressive Formal Model of the Web Infrastructure (Short)
Marcus Völker
Heuristiken und Modellierungen für die Wertebereichsanalyse von Steuerungssoftware mit Policy Iteration
Im Bereich der statischen Programmanalyse ist die Wertebereichsanalyse ein
wichtiges Werkzeug, um Wertebereiche für Programmvariablen abzuschätzen. Ein
Algorithmus für die Wertebereichsanalyse ist die sogenannte Policy Iteration,
bei der das Programm mittels einer Heuristik in ein einfacher zu analysierendes
Programm transformiert wird. Dieses wird dann mit einem Standardansatz wie z.B.
Fixpunktiteration analysiert und die Ergebnisse auf Korrektheit in Bezug auf das
ursprüngliche Programm getestet. Sollten die Ergebnisse inkorrekt sein, werden
andere Vereinfachungen ausprobiert, bis korrekte Ergebnisse erzielt werden. Da
die Standardheuristik bei der Programmtransformation bestimmte Annahmen über das
Programm trifft, ist es möglich, eine bessere Heuristik zu konstruieren, wenn
zuerst eine Voranalyse feststellt, ob diese Annahmen korrekt sind oder nicht und
eine auf die gefundenen Programmeigenschaften passende Transformation auswählt.
Ein weiteres Thema ist die Modellierung des Eingabeprogramms auf eine Art und
Weise, sodass die Heuristik angewandt werden kann. Hierbei werden beispielsweise
polynomielle Ungleichungen, die im Programm als Schleifenbedingungen vorkommen,
umgeformt und durch lineare Ungleichungen approximiert werden, die die Heuristik
behandeln kann.
Alexander Weigl
Provably Forgetting of Information in Manufacturing Systems (Short)
During the manufacturing process, information are generated and aggregated
that constitute a business secrets and therefore need a high protection. On
the other hand, if we can prove, that an information is absented, the effort
for the protection for this system could be invested on different
information, aspects or systems.
For this, we develop the notion of information forgetting of a reactive
system. This notion describes that a reactive system needs to forget the
information about a secret within a certain amount of cycles. This property
limits the amount of historical information an attacker can learn by
observing a manufacturing system. Moreover, we formalise and prove the
notion of an
information forgetting system with
Relational Test
Tables.
We evaluate the verification on the industry demonstrator for KASTEL SVI
project, which was provided by the Fraunhofer IOSB and developed by
industrial third-party contractor. In this demonstrator, we are able to
show, that a selected business secret &endash; the number of wheel turns
&endash; is not forgotten. We suggest and prove a fix of the leak.
We close with an elaborate discussion on the verification and results and
also with remarks to the how
information forgetting relates supports
quantifiable security.
