Reliably Secure Software Systems (RS3) –
DFG Priority Programme 1496

Annual Meeting 2014 (October 7-10, 2014)

Overview

The fourth annual meeting of RS3 took place from 7th to 10th of October 2014. On October 7th and 8th the projects presented their current status and the next steps of RS3 were planned. This part of the meeting was directly followed by a two-day staff meeting on October 9th and 10th.  The staff meeting was intended for work on RS3-wide, common topics. The meeting took place in Trier.

Date and Location

Members of the scientific advisory board were invited to attend:
07.10.2014 - 08.10.2014.

Members of the Friends of RS3 (FoRS3) were invited to attend:
07.10.2014 - 08.10.2014.

Principal investigators of RS3 projects were invited to attend:
07.10.2014 - 08.10.2014.

Doctoral and post-doctoral researchers in RS3 projects were invited to attend:
07.10.2014 - 10.10.2014.

The meeting took place at:

Universität Trier
Behringstraße 21
54296 Trier

The sessions on October 7 and 8 took place in building H room HS 13. The website of Universität Trier provides directions to the university as well as an overview of the rooms.

Schedule

During the annual meeting the progress of individual projects as well as of RS3 as a whole was presented. During the staff meeting the post-doctoral and doctoral researchers worked on common topics in the reference scenarios and project clusters.

The schedule for the meeting can be found here

Keynote Talk by Andrei Sabelfeld: Securing Web Applications

Web application security is concerned with protecting information as it is manipulated by web applications. This is an important area because attacks against web applications constitute more than 60% of the total attack attempts observed on the Internet, according to recent surveys. This talk makes a case for a principled approach to web application security, which enables the enforcement of versatile confidentiality and integrity policies by construction. We showcase a selection of recent achievements on tracking information flow in web applications and overview some cutting-edge ongoing work on securing web mashups and on end-to-end web application security.

Keynote Talk by Stephan Zdancewic: Vellvm: Verifying Safety in the LLVM IR

The Low-Level Virtual Machine (LLVM) compiler provides a modern, industrial-strength SSA-based intermediate representation (IR) along with infrastructure support for many source languages and target platforms. Much of the LLVM compiler is structured as IR to IR translation passes that apply various optimizations and analyses, making it an ideal target for enforcing security properties of low-level code.

In this talk, I will describe the Vellvm project, which seeks to provide a formal framework for developing machine-checkable proofs about LLVM IR programs and translation passes. I'll discuss some of the subtleties of modeling the LLVM IR semantics, including nondeterminism and its use of SSA representation. I'll also describe some of the proof techniques that we have used for reasoning about LLVM IR transformations and describe our results about the formal verification of the SoftBound pass, which hardens C programs against memory safety errors.

Vellvm, which is implemented in the Coq theorem prover, provides facilities for extracting LLVM IR transformation passes and plugging them into the LLVM compiler, thus enabling us to create verified optimization passes for LLVM and evaluate them against their unverified counterparts. Our experimental results show that fully verified and automatically extracted implementations can yield competitive performance.

This is joint work with Jianzhou Zhao and Milo Martin (both at Penn) and Santosh Nagarakatte (at Rutgers University).

Accommodation and Reimbursement

Please use the following travel claim forms for your reimbursement:

English explanation of the travel claim form: pdf version

Contact

If you have further questions regarding the annual meeting, please do not hesitate to contact
assistant at spp-rs3.de.