News: Grants

Krishna Gummadi and Alan Mislove awarded a Facebook “Secure the Internet” grant

October 23, 2018

MPI-SWS faculty member Krishna Gummadi and MPI-SWS alumnus Alan Mislove have been awarded a "Secure the Internet" grant by Facebook. Their proposal, “Towards privacy-protecting aggregate statistics in PII-based targeted advertising,” has been awarded $60,000 to develop techniques for revealing advertising statistics that provide hard guarantees of user privacy, based on a (principles-first) approach. Their goal is to develop a differential privacy-like approach that can be applied to existing advertising systems.

The Facebook "Secure the Internet" grant program is designed to improve the security,

MPI-SWS faculty member Krishna Gummadi and MPI-SWS alumnus Alan Mislove have been awarded a "Secure the Internet" grant by Facebook. Their proposal, “Towards privacy-protecting aggregate statistics in PII-based targeted advertising,” has been awarded $60,000 to develop techniques for revealing advertising statistics that provide hard guarantees of user privacy, based on a (principles-first) approach. Their goal is to develop a differential privacy-like approach that can be applied to existing advertising systems.

The Facebook "Secure the Internet" grant program is designed to improve the security, privacy, and safety of internet users. Gummadi and Mislove's proposal was one of only 10 winning proposals, which were together awarded more than $800,000 by Facebook.

Read more

Maria Christakis receives Facebook Faculty Research Award

December 15, 2017

Maria Christakis, an MPI-SWS faculty member, has received a Facebook Faculty Research Award. The award is given in recognition of Maria's work on combining static and dynamic program analysis, which is of particular relevance to Facebook as they are developing sophisticated program analysis tools to handle real-world code.

Two MPI-SWS faculty awarded DFG grants

December 14, 2017

Two MPI-SWS faculty members have received 3-year research grants from DFG, the German Research Organization.

Eva Darulova has received a single-PI DFG grant entitled "Automated Rigorous Verification and Synthesis of Approximations." Björn Brandenburg has received a DFG grant entitled "RT-Proofs: Formal proofs for real-time systems." This award is for a collaborative grant, with co-PIs at INRIA (Grenoble), Verimag (Grenoble), ONERA (Toulouse), and TU Braunschweig (Germany).

Both projects are actively recruiting doctoral students.

Two MPI-SWS faculty members have received 3-year research grants from DFG, the German Research Organization.

Eva Darulova has received a single-PI DFG grant entitled "Automated Rigorous Verification and Synthesis of Approximations." Björn Brandenburg has received a DFG grant entitled "RT-Proofs: Formal proofs for real-time systems." This award is for a collaborative grant, with co-PIs at INRIA (Grenoble), Verimag (Grenoble), ONERA (Toulouse), and TU Braunschweig (Germany).

Both projects are actively recruiting doctoral students. Interested students can apply online.

Automated Rigorous Verification and Synthesis of Approximations

Computing resources are fundamentally limited and sometimes an exact solution may not even exist. Thus, when implementing real-world systems, approximations are inevitable, as are the errors introduced by them. The magnitude of errors is problem-dependent but higher accuracy generally comes at a cost in terms of memory, energy or runtime, effectively creating an accuracy-efficiency tradeoff. To take advantage of this tradeoff, we need to ensure that the computed results are sufficiently accurate, otherwise we risk disastrously incorrect results or system failures. Unfortunately, the current way of programming with approximations is mostly manual, and consequently costly, error prone and often produces suboptimal results.

The goal of this project is to develop an end-to-end system which approximates numerical programs in an automated and trustworthy fashion. The programmer will be able to write exact high-level code and our `approximating compiler' will generate an efficient implementation satisfying a given accuracy specification. In order to achieve this vision, we will develop novel sound techniques for verifying the accuracy of approximate numerical programs, as well as new synthesis approaches to generate such approximations automatically.

RT-Proofs: Formal proofs for real-time systems

Real-time systems, i.e., computer systems subject to stringent timing constraints, are at the heart of most modern safety-critical technologies, including automotive systems, avionics, robotics, and factory automation, to name just a few prominent domains in which incorrect timing can have potentially catastrophic consequences. To assure the always-correct operation of such systems, i.e., to make sure that they always react in a timely fashion even in a worst-case scenario, rigorous validation efforts are required prior to deployment. However, establishing that all timing constraints are met is far from trivial --- and requires sophisticated analysis techniques --- because software timing varies in complex and difficult to predict ways, e.g., due to scheduling delays, shared resources, or communication, even when executing on a dedicated processor. Unfortunately, the theoretical foundations of current analysis methods are not nearly as rock-solid as one might expect.

The key problem is that the state-of-the-art methods are backed by only informal or abbreviated proofs, which are typically difficult to understand, check, adapt, or reuse. As a result, there is a non-trivial risk of subtle, but fatal mistakes, either lingering in the published literature, or arising when combining results with unstated, inconsistent assumptions. And indeed, this is not just a hypothetical concern --- most famously, the timing analysis of the CAN real-time bus (widely deployed in virtually all modern cars) was refuted in 2007, 13 years after initial publication. Similarly, other lesser-known examples of incorrect worst-case analyses abound in the literature, including off-by-one errors, incorrect generalizations, and even claims that are simply wrong. Worse, even if the underlying theory is indeed flawless, there is still no guarantee that it is actually implemented correctly in the toolchains used in practice. In short, the state of the art in the analysis of safety-critical real-time systems leaves a lot to be desired --- informal "pen and paper" proofs are simply inadequate.

There is a better way: timing analysis results should be formally proved, machine-checkable, and independently verifiable. To this end, the RT-proofs project will lay the foundations for the computer-assisted verification of schedulability analysis results by (i) formalizing foundational real-time concepts using the Coq proof assistant and (ii) mechanizing proofs of busy-window-based end-to-end latency analysis, the analysis approach of greatest practical relevance (e.g., used by SymTA/S). Additionally, we will (iii) demonstrate with a practical prototype how trust in a vendor's toolchain can be established by certifying the produced analysis results (rather than the tool itself). Leading by example, RT-proofs will fundamentally raise the level of rigor, to the benefit of the academic community, tool vendors, and real-time systems engineers in practice.

Read more

Peter Druschel and Deepak Garg receive funding from Google

February 1, 2014

MPI-SWS faculty members Peter Druschel and Deepak Garg have received a Google Faculty Research Award. The award is conferred on selected recipients, based on proposals from all over the world. The award, granted in the area of computer systems, supports their work on enforcing declarative data policies in distributed systems.

Derek Dreyer wins funding from Microsoft Research

May 1, 2013

A research project proposed by MPI-SWS faculty member Derek Dreyer has been selected for a 2013 Microsoft Research PhD Scholarship. The project is entitled "Compositional Verification of Scalable Joins by Protocol-Based Refinement". Each year Microsoft selects approximately twenty projects to fund, based on proposals from research institutions across Europe, Africa, and the Middle East. The Scholarship funds a PhD student for three years.