RV 2017 will feature the following invited speakers.
Brown University, USA
Title and abstract TBA
Rodrigo Fonseca is an assistant professor at Brown University’s Computer Science Department. He holds a PhD from UC Berkeley, and prior to Brown was a visiting researcher at Yahoo! Research. He is broadly interested in networking, distributed systems, and operating systems, and is the recipient of an NSF CAREER award, and of a 2015 SOSP Best Paper Award. His research involves seeking better ways to build, operate, and diagnose distributed and networked systems.
Vladimir Levin and Jakob Lichtenberg
Title: Windows Driver Verification Platform
The Windows Driver Verification Platform (DVP) provides compile time and runtime technologies for verifying that device drivers work correctly: Static Driver Verifier (SDV) is a compile time verification tool available for 3rd party developers as part of the Windows Driver Development kit. Runtime Driver Verifier (DV) is integrated directly into the Windows OS and shipped inbox. Both technologies are used by 3rd party driver developers as well as internally at Microsoft and in the entire range of Window devices from IoT devices and all the way up to Microsoft Azure deployments.
Whereas verification paradigms, engines, and abilities are different between SDV and DV, these technologies share a common concept of interface rules between the OS kernel and drivers (kernel extensions, in general). The interface is materialized by a set of APIs supplied by the kernel and sets of callbacks supplied by drivers. In a narrow sense, each of the two technologies is aimed at verifying that drivers follow the interface rules.
The talk will cover the current state of the platform, shared features of the two technologies and their differences. We will also discuss our pipeline for technology transfer from Microsoft Research to Windows.
Vladimir Levin is a Principal Software Design Engineer in the Microsoft Windows and Devices Group, and the technical lead of the eXtensible Driver Verifier and Test in Production through Driver Verifier projects, and co-leading the Static Driver Verifier project. Vladimir received his PhD in Computer Science from Lomonosov Moscow State University. In Russia, he worked at the Keldysh Institute of Applied Mathematics, Moscow, where he was engaged in the Russian Airspace space shuttle Buran project: he participated in designing a programming language for development of ground control & test software, and implemented the runtime support for it. Before joining Microsoft, he worked at the Bell Laboratories on technology transfer of the FormalCheck hardware verification tool, and was engaged in a software-hardware co-verification research.
Jakob Lichtenberg works at Microsoft in the Windows Device Platform group. Jakob is dev lead for the Windows Driver Kit and for the Driver Quality Tools team that among other tools, builds Static Driver Verifier and Runtime Driver Verifier to allow driver developers to build high quality device drivers for the Windows platform. Jakob graduated from Technical University of Denmark with a MSc, where his research was focused on model checking techniques for formal verification of hybrid and timed systems. In continuation of this research Jakob co-founded a Danish IT startup configit.com< that invented the application of model checking techniques to allow seamless large-scale product customization. Jakob was among the first to join the PhD program at the IT University of Copenhagen, but ultimately ended up with a job at Microsoft in Seattle rather than a doctorate.
Saarland University, Germany
Title: Learning Input Languages for Runtime Verification
Let us use dynamic tainting to follow the paths of input characters through a program. We will then see that some input fragments end in some variables, and others in others. This allows us to decompose the input into individual parts, one per variable, and consequently, to infer the entire structure of the input as a context-free grammar. In the context of runtime verification, such inferred input grammars have a number of uses. First, they can be used as test drivers, allowing to cover millions of executions in minutes. Second, they can serve to derive dynamic invariants, such as pre- or postconditions. Third, grammars, as well as invariants, can be easily verified dynamically, checking whether inputs and invariants conform to the learned languages. The AUTOGRAM approach will be demonstrated using examples of real programs and (if time permits) even live coding on stage.
Andreas Zeller is a full professor for Software Engineering at Saarland University in Saarbrücken, Germany. His research concerns the analysis of complex software systems, their security properties, and their development process. His students are funded by companies like Google, Microsoft, or SAP. In 2010, Zeller was inducted as Fellow of the ACM for his contributions to automated debugging and mining software archives. In 2011, he received an ERC Advanced Grant, Europe’s highest and most prestigious individual research grant, for work on specification mining and test case generation. In 2013, he co-founded Testfabrik AG, a start-up for automatic testing of Web applications.