MAIS Kickoff Meeting for Labs and Seminars, SoSe2019

[Gheraccio]

Dear Students,

we are excited to inform you that the Modeling and Analysis of Information Systems chair (http://www.mais.informatik.tu-darmstadt.de/), held by Professor Heiko Mantel, will offer two seminars and two labs on different topics from prolific and research-active fields of computer science.

OUR OFFER (you will find a brief description of each module below):

- Seminar: Current Topics in Secure Usage
- Seminar: Side-Channel Attacks on Software
- Lab Course: Dynamic Enforcement for Software Security
- Lab Course: Formal Specification and Verification in Isabelle/HOL

Please come and meet the team at the Kick-Off Meeting, where the modules will be presented:
Thursday, 18.04.2019, 15:20 in room S2|02 A213

Looking forward to seeing you there!

Yours truly,
the MAIS Team

---------------------------------
Seminars and Labs Description
---------------------------------

Seminar: Current Topics in Secure Usage
Contact person: Tobias Hamann

Users entrust applications with an increasing amount of sensitive data.
Malicious or faulty applications processing this data can cause
substantial harm to users' information security and privacy. One option
for mitigating this risk are usage control mechanisms that can be used
to specify and control the desired terms of data usage by applications.
In this seminar course, we discuss recent research papers on usage
control published at top conferences. Each paper is presented by one
participant and is then discussed in detail by the entire group of
participants. Exemplary topics covered in the discussed articles include:

* access and usage control mechanisms (e.g., for IoT devices);
* recent attacks and countermeasures;
* mechanisms for detecting security violations;
* mechanisms for monitoring system executions.


Seminar: Side-Channel Attacks on Software
Contact people: Tobias Hamann, Alexandra Weber

Side channels are unintended indirect flows of information revealed by
physical executions of a computer program. Examples of side channels
include program's running time, cache behavior, power consumption,
electromagnetic or acoustic emanation, etc. Such unintended flows of
information can be correlated to secrets e.g., private cryptographic
keys, and this makes side channels a severe security vulnerability.
During a side-channel attack the hacker collects the information
revealed through side channels, carefully analyzes this information, and
recovers the secrets from it. Due to improvements in security protection
mechanisms traditional security vulnerabilities like programming bugs
are getting harder to exploit, and that is why side channels are
becoming now more and more attractive to hackers.

In this seminar we will discuss research articles on different aspects
of side-channel attacks on software as well as countermeasures against
them. Exemplary topics include:

* side-channel attacks on cryptographic software;
* side-channel attacks on web applications;
* side-channel attacks on operating systems;
* side-channel attacks on mobile devices;
* side-channel attacks in the cloud.


Lab Course: Dynamic Enforcement for Software Security
Contact people: Yuri Gil Dantas, Tobias Hamann

Dynamic enforcement is a technique for achieving security by monitoring
an application's runtime behavior and applying suitable countermeasures
when necessary. This lab course introduces the concept of dynamic
enforcement for Java programs. Of particular relevance for today's
information security are distributed applications like cloud storage.
Dynamic enforcement for distributed applications is the focus of this
lab course. The topics covered by this lab course include:

* introduction to tools for dynamic monitoring and enforcement like
CliSeAu, JavaMOP and Polymerm;
* specification of security requirements in different formalisms;
* combination of mechanisms for dynamic monitoring and enforcement with
target programs, in particular using inlining;
* basic concepts of dynamic monitoring and enforcement in distributed
systems;
* central vs decentralized monitoring and enforcement in distributed systems;
* protocols for coordinating actions of decentralized mechanisms.


Lab Course: Formal Specification and Verification in Isabelle/HOL
Contact people: Lorenzo Gheri, Tobias Hamann

Formal methods allow one to model critical requirements precisely and to
certify with mathematical rigor that such requirements are met by a
system. For applying formal methods to real world problems, tool support
is essential. This lab course introduces how to use the Isabelle/HOL
tool that is one of the internationally leading tools. Formal models of
increasing conceptual complexity will be defined in Isabelle's
higher-order logic, so that Isabelle's semi-automatic verification
engine may subsequently be used to verify the desired properties. The
topics covered by this course include:

* techniques for modeling systems in higher-order logic;
* techniques for specifying desired systems properties;
* design of formal models for systems;
* evaluation of advantages and disadvantages of a chosen model.

[Gheraccio]

Hello Students,

please don't miss the opportunity to attend the seminars and labs
offered by MAIS! These will focus on different topics from prolific and
research-active fields of computer science:

- Seminar: Current Topics in Secure Usage
http://www.mais.informatik.tu-darmstadt ... -ss19.html
- Seminar: Side-Channel Attacks on Software
http://www.mais.informatik.tu-darmstadt ... -ss19.html
- Lab Course: Dynamic Enforcement for Software Security
http://www.mais.informatik.tu-darmstadt ... o-lab-ss19
- Lab Course: Formal Specification and Verification in Isabelle/HOL
http://www.mais.informatik.tu-darmstadt ... -ss19.html

If interested please attend the kickoff meeting tomorrow, Thursday
18.04.2019, at 15:20 in room S2|02 A213. Should you not be able to
attend the kickoff meeting, please inform as soon as possible the
contact person of the lab or seminar you are interested in!

Looking forward to seeing you tomorrow!

Yours truly,
the MAIS Team