Upcoming events

Type-Driven Program Synthesis

Nadia Polikarpova
MIT CSAIL, Cambridge USA
SWS Colloquium
15 Feb 2017, 10:00 am - 11:00 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Modern programming languages safeguard developers from many typical errors yet more subtle errors-such as violations of security policies-still plague software. Program synthesis has the potential to eliminate such errors by generating executable code from concise and intuitive high-level specifications. Traditionally program synthesis failed to scale to specifications that encode complex behavioral properties of software: these properties are notoriously hard to check even for a given program and so it?s not surprising that finding the right program within a large space of candidates has been considered very challenging. My work tackles this challenge through the design of synthesis-friendly program verification mechanisms which are able to check a large set of candidate programs against a complex specification at once whereby efficiently pruning the search space.

Based on this principle I developed Synquid a program synthesizer that accepts specifications in the form of expressive types and uses a specialized type checker as its underlying verification mechanism. Synquid is the first synthesizer powerful enough to automatically discover provably correct implementations of complex data structure manipulations such as insertion into Red-Black Trees and AVL Trees and normal-form transformations on propositional formulas. Each of these programs is synthesized in under a minute. Going beyond textbook algorithms I created a language called Lifty which uses type-driven synthesis to automatically rewrite programs that violate information flow policies. In our case study Lifty was able to enforce all required policies in a prototype conference management system.

Adventures in Systems Reliability: Replication and Replay

Ali Mashtizadeh
Stanford University
SWS Colloquium
17 Feb 2017, 10:30 am - 1:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
The past decade has seen a rapid acceleration in the development of new and transformative applications in many areas including transportation medicine ?nance and communication. Most of these applications are made possible by the increasing diversity and scale of hardware and software systems. While this brings unprecedented opportunity it also increases the probability of failures and the dif?culty of diagnosing them. Increased scale and transience has also made management increasingly challenging. Devices can come and go for a variety of reasons including mobility failure and recovery and scaling capacity to meet demand. In this talk I will be presenting several systems that I built to address the resulting challenges to reliability management and security. Ori is a reliable distributed ?le system for devices at the network edge. Ori automates many of the tasks of storage reliability and recovery through replication taking advantage of fast LANs and low cost local storage in edge networks. Castor is record/replay system for multi-core applications with predictable and consistently low overheads. This makes it practical to leave record/replay on in production systems to reproduce difficult bugs when they occur and to support recovering from hardware failures through fault tolerance. Cryptographic CFI (CCFI) is a dynamic approach to control flow integrity. Unlike previous CFI systems that rely purely on static analysis CCFI can classify pointers based on dynamic and runtime characteristics. This limits the attacks to only actively used code paths resulting in a substantially smaller attack surface.

Safe, Real-Time Software Reference Architectures for Cyber-Physical Systems

Renato Mancuso
University of Illinois at Urbana- Champaign
SWS Colloquium
21 Feb 2017, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Renato Mancuso is a doctoral candidate in the Department of Computer Science at the University of Illinois at Urbana-Champaign. He is interested in high-performance cyber-physical systems with a specific focus on techniques to enforce strong performance isolation and temporal predictability in multi-core systems. He has published around 20 papers in major conferences and journals. His papers were awarded a best student paper award and a best presentation award at the Real-Time and Embedded Technology and Applications Symposium (RTAS) in 2013 and 2016 respectively. He was the recipient of a Computer Science Excellence Fellowship and a finalist for the Qualcomm Innovation Fellowship. Some of the design principles for real-time multi-core computing proposed in his research have been officially incorporated in recent certification guidelines for avionics systems. They have also been endorsed by government agencies industries and research institutions worldwide. He received a B.S. in Computer Engineering with honors (2009) and a M.S. in Computer Engineering with honors (2012) from the University of Rome "Tor Vergata".

Recent events

On the Security and Scalability of Proof of Work Blockchains

Arthur Gervais
ETH Zurich
SWS Colloquium
08 Feb 2017, 10:00 am - 12:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
The security properties of blockchain technology allow for the shifting of trust assumptions e.g. to remove trusted third parties; they however create new challenges for security and scalability which have not yet been fully understood and that we investigate in this talk. The blockchain?s security for example affects the ability of participants to exchange monetary value or to participate in the network communication and the consensus process. Our first contribution provides a quantitative framework to objectively compare the security and performance characteristics of Proof of Work-based blockchains under adversaries with optimal strategies. Our work allows us to increase Bitcoin?s transaction throughput by a factor of ten given only one parameter change and without deteriorating the security of the underlying blockchain. In our second contribution we highlight previously unconsidered impacts of the PoW blockchain?s scalability on its security and propose design modifications that are now implemented in the primary Bitcoin client. Because blockchain technology is still in its infancy we conclude the talk with an outline of future work towards an open scalable privacy-preserving and decentralized blockchain.

Guiding program analyzers toward unsafe executions

Dr. Maria Christakis
University of Kent
SWS Colloquium
06 Feb 2017, 10:00 am - 11:00 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Most static program analysis techniques do not fully verify all possible executions of a program. They leave executions unverified when they do not check certain properties fail to verify properties or check properties under certain unsound assumptions such as the absence of arithmetic overflow. In the first part of the talk I will present a technique to complement partial verification results by automatic test case generation. In contrast to existing work our technique supports the common case that the verification results are based on unsound assumptions. We annotate programs to reflect which executions have been verified and under which assumptions. These annotations are then used to guide dynamic symbolic execution toward unverified program executions leading to smaller and more effective test suites.

In the second part of the talk I will describe a new program simplification technique called program trimming. Program trimming is a program pre-processing step to remove execution paths while retaining equi-safety (that is the generated program has a bug if and only if the original program has a bug). Since many program analyzers are sensitive to the number of execution paths program trimming has the potential to improve their effectiveness. I will show that program trimming has a considerable positive impact on the effectiveness of two program analysis techniques abstract interpretation and dynamic symbolic execution.

Inverse Rendering

Shida Beigpour
Joint Lecture Series
01 Feb 2017, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
Photographs as well as video frames are two-dimensional projections of three-dimensional real-world scenes. Photorealistic Computer Graphic Imagery (CGI) is usually generated by "rendering" a sophisticated three-dimensional model of a realistic scene on to a virtual camera sensor. Such process is not invertible due to the high amount of data loss. Still both physically captured photographs and synthesized photos (CGI) contain considerable amount of information about the characteristics of the scene itself. Even naïve human viewers are able to infer important information about the scene e.g. shape material illumination distance and actions solely from a single image. This is indeed much more difficult for computer systems. Inverse rendering is one of the hot-topics in computer vision in which the goal is to estimate and model the three-dimensional scene and its illumination automatically given only one or a sparse set of images from the scene. This is by nature a highly under-constraint problem which makes it very complex to solve. Yet the advancements in computation and imaging technologies (e.g. depth sensors and light-field cameras) open new horizons in this field. Inverse rendering makes many interesting applications possible including: creating novel views of the scene/objects re-lighting detecting and altering the object materials in the photographs and augmented reality.  This talk provides a brief overview of some of the state-of-the-art inverse rendering techniques and datasets with a strong focus on addressing the complexities of real-world scenarios.