Masking schemes are widely used in practice to defeat side-channel attacks, which exploit the power consumption of devices. At the same time a large body of recent theoretical works study feasibility of computation in the presence of leakage and attempts to provide a formal security analysis of the masking countermeasure. In this talk, we will review some recent advances in the formal security analysis of masking schemes and present efficient ways how to apply the masking countermeasure at smart card level.

In this talk, we give an overview of three recent studies on advanced web tracking mechanisms, namely browser fingerprinting, evercookies and cookie syncing. These tracking mechanisms can be differentiated from their conventional counterparts (e.g. cookies) by their potential to circumvent users' tracking preferences, being hard to discover and resilient to removal. We will present the results from our large-scale analysis of font-based fingerprinting (CCS'13), canvas fingerprinting, evercookies and cookie syncing (CCS'14). Moreover, we present our work on HTML5 Battery Status API (DPM'15), which highlighted the privacy risks associated with the API. These include short term tracking by battery information and exploiting the high precision readouts provided by Firefox on Linux to discover the capacity of users' batteries.

In biometric authentication protocols, a user is authenticated or granted access to a service if her fresh biometric trait matches the reference biometric template stored on the service provider. This matching process is usually based on a suitable distance which measures the similarities between the two biometric templates. In this talk, we prove that, when the matching process is performed using a specific family of distances, then information about the reference template is leaked. We show how it is possible to perform a template recovery attack even in privacy-preserving biometric authentication protocols and we formalise this "leakage of information" in a mathematical framework.

The cardinality operator is indispensable when specifying and reasoning about parameterized concurrent/distributed systems. It provides a level of abstraction and conciseness that makes (manual) proofs go through smoothly. Unfortunately, the automation support for such proofs remains elusive due to challenges in counting sets of unbounded program states. In this talk, I will present #Π a tool that can automatically synthesize cardinality-based proofs of parameterized systems. #Π crucially relies on a sound and precise axiomatization of cardinality for the combined theory of linear arithmetic and arrays. This axiomatization is the key technical contribution of this work. We show that various parameterized systems, including mutual exclusion and consensus protocols, can be efficiently verified using #Π. Many of them were automatically verified for the first time. This is joint work with Nikolaj Bjørner and Andrey Rybalchenko.

We present two semantic views of probabilistic programs and their relationship. An operational interpretation as well as a weakest precondition semantics are provided for an elementary probabilistic guarded command language. Our study treats features such as random sampling, conditioning, loop divergence, and non-determinism.

We then discuss two key analysis problems: almost-sure termination (does a program terminate with probability one?) and loop invariant synthesis.

In this talk, we will describe progress on computing invariants involving expected values of program variables in probabilistic programs that combine imperative programs with random number generation constructs. Such invariants can express properties such as "for any loop iteration, the average value of x is less than the average of y". We will first examine a proof system for such invariants, culminating in a fixed point characterization. We then show how such fixed points can indeed be computed using abstract interpretation, presenting a prototype static analysis that realizes our ideas using the polyhedral abstract domain. We conclude by examining connections between our fixed points and concepts in martingale theory.

Joint work with Aleksandar Chakarov.

I'll present the first stages of an investigation into how simple we can get away with making the foundations of modular correctness reasoning for shared-memory concurrent programs. Today's most popular tools for this problem are program logics, but we adopt a different approach, within the Coq proof assistant. Namely, as the core of the framework, we define a simple instrumented operational semantics with one kind of ghost state: monitors, a kind of process that observes execution and enforces adherence to a protocol. On that foundation, we develop some "opt-in" machinery in service of proving stylized correctness theorems. We define connectives and rules for deriving correctness of programs. With our Coq implementation, we have verified a Treiber lock-free stack and a Harris-Michael lock-free set, as well as client programs, proved mostly automatically and parametrically in implementation details of the data structures.

This is joint work with C.J. Bell, Mohsen Lesani, Gregory Malecha, Stephan Boyer, and Peng Wang.

Automated unit test generation tools can produce tests that are superior to manually written ones in terms of code coverage, but are these tests helpful to developers while they are writing code? A developer would first need to know when and how to apply such a tool, and would then need to understand the resulting tests in order to provide test oracles and to diagnose and fix any faults that the tests reveal. Considering all this, does automatically generating unit tests provide any benefit over simply writing unit tests manually?

We empirically investigated the effects of using an automated unit test generation tool (EVOSUITE) during development. A controlled experiment with 41 students shows that using EVOSUITE leads to an average branch coverage increase of 13%, and 36% less time is spent on testing compared to writing unit tests manually. However, there is no clear effect on the quality of the implementations, as it depends on how the test generation tool and the generated tests are used. In-depth analysis, using five think-aloud observations with professional programmers, confirms the necessity to increase the usability of automated unit test generation tools, to integrate them better during software development, and to educate software developers on how to best use those tools.

Joint work with Gordon Fraser and Andrea Arcuri. Accepted for publication and to be presented at ISSTA'15.

Achieving high structural coverage is an important aim in software testing. Several search-based techniques have proved successful at automatically generating tests that achieve high coverage. However, despite the well- established arguments behind using evolutionary search algorithms (e.g., genetic algorithms) in preference to random search, it remains an open question whether the benefits can actually be observed in practice when generating unit test suites for object-oriented classes. In this paper, we report an empirical study on the effects of using a genetic algorithm (GA) to generate test suites over generating test suites incrementally with random search, by applying the EvoSuite unit test suite generator to 1,000 classes randomly selected from the SF110 corpus of open source projects. Surprisingly, the results show little difference between the coverage achieved by test suites generated with evolutionary search compared to those generated using random search. A detailed analysis reveals that the genetic algorithm covers more branches of the type where standard fitness functions provide guidance. In practice, however, we observed that the vast majority of branches in the analyzed projects provide no such guidance.

Joint work with Jose Miguel Rojas, Gordon Fraser and Phil McMinn. Accepted for publication and to be presented at GECCO'15.

In this, we tackle the problem of the existence of solutions for recursive systems of Horn clauses with second-order variables interpreted as integer relations, and harnessed by quantifier-free difference bounds arithmetic. We start by proving the decidability of the problem "does the system have a solution ?" for a simple class of Horn systems with one second-order variable and one non-linear recursive rule. The proof relies on a construction of a tree automaton recognizing all cycles in the weighted graph corresponding to every unfolding tree of the Horn system. We constrain the tree to recognize only cycles of negative weight by adding a Presburger formula that harnesses the number of times each rule is fired, and reduce our problem to the universality of a Presburger-constrained tree automaton. We studied the complexity of this problem and found it to be in NEXPtime with an EXPtime-hard lower bound. Second, we drop the univariate restriction and consider multivariate second-order Horn systems with a structural restriction, called flatness. This more general class of Horn systems is found to be decidable, within the same complexity bounds. Finally, we encode the reachability problem for Alternating Branching Vector Addition Systems (ABVASS) using Horn systems and prove that, for flat ABVASS, this problem is in co-NEXPtime. Link: http://fr.arxiv.org/abs/1503.00258

Online services often use replication for improving the performance of user-facing services. However, using replication for performance comes at a price of weakening the consistency levels of the replicated service. To address this tension, recent proposals from academia and industry allow operations to run at different consistency levels. In these systems, the programmer has to decide which level to use for each operation. We present SIEVE, a tool that relieves Java programmers from this error-prone decision process, allowing applications to automatically extract good performance when possible, while resorting to strong consistency whenever required by the target semantics. Taking as input a set of application-specific invariants and a few annotations about merge semantics, SIEVE performs a combination of static and dynamic analysis, offline and at runtime, to determine when it is necessary to use strong consistency to preserve theseinvariants and when it is safe to use causally consistent commutative replicated data types (CRDTs). We evaluate SIEVE on two web applications and show that the automatic classification overhead is low.

If time permits, I will also briefly introduce our work in progress, which addresses limitations of existing multi-level consistency proposals and minimizes the coordination in replicated systems. In this work, we first define the consistency semantics of various operations as visibility restrictions between operations. Second, we build a replication and coordination middleware to efficiently execute and replicate operations with respect to their corresponding restrictions.

This is a joint work with Rodrigo Rodrigues (Instituto Superior Tecnico, Lisbon), Allen Clement (MPI-SWS/Google), Nuno Preguica (Nova University of Lisbon), Viktor Vafeiadis (MPI-SWS) and Joao Leitao (Nova University of Lisbon).

Software is sometimes redundant, in the sense that some operations are designed to behave like others but their executions differ. This redundancy can be either deliberately introduced, as in the case of N-version programming, or intrinsically present due to common design and development practices.

In this talk we present the notion of intrinsic redundancy, we show that it exists and is pervasive in software systems, and we argue that it can be exploited to improve the reliability of a system, and to enhance software testing.

Intrinsic redundancy has been manually identified, so far. We present a search-based technique that can effectively and efficiently extract intrinsic redundancy from the source code of a given software.

We then describe a technique to automatically generate test oracles from intrinsic software redundancy. We also present the results of an experimental evaluation showing that such oracles can be quite effective in reveling faults with automatically generated tests and that they can even improve good hand-written test suites.

We propose a framework to prove almost sure termination for probabilistic programs with real valued variables. It is based on ranking supermartingales, a notion analogous to ranking functions on nonprobabilistic programs. The framework is proven sound and complete for a meaningful class of programs involving randomization and bounded nondeterminism. We complement this foundational insight by a practical proof methodology, based on sound conditions that enable compositional reasoning and are amenable to a direct implementation using modern theorem provers. This is integrated in a small dependent type system, to overcome the problem that lexicographic ranking functions fail when combined with randomization. Among others, this compositional methodology enables the verification of probabilistic programs outside the complete class that admits ranking supermartingales.

Modern test generation techniques allow to generate as many executions as needed; combined with dynamic analysis, they allow for understanding program behavior in situations where static analysis is challenged or impossible. However, all these dynamic techniques would still suffer from the incompleteness of testing: If some behavior has not been observed so far, there is no guarantee that it may not occur in the future. In this talk, I introduce a method called Test Complement Exclusion that combines test generation and sandboxing to provide such a guarantee. Test Complement Exclusion will have significant impact in the security domain, as it effectively detects and protects against unexpected changes of program behavior; however, guarantees would also strengthen findings in dynamic software comprehension. First experiments on real-world ANDROID programs demonstrate the feasibility of the approach; details are available on http://www.boxmate.org/.

Set up by the European Union in 2007, the European Research Council (ERC) is implementing its second work program in H2020. The achievements of these eight years of successful operations as well as the structure of ERC funding schemes foreseen in Work Programme 2015 will be presented. Emphasis will be made on the type of research funded, the proposal submission process, the evaluation procedure and the features of the ERC grants.

The progress in microelectronics has enabled the miniaturization of processing elements, radio transceivers, and sensing elements of a large array of physiological phenomena. This situation has made plausible to realize low cost, low power, miniaturized, yet smart sensor nodes needed to develop wireless body-area sensor networks (WBSN). However, the inherent resource-constrained nature of these systems, coupled with the harsh operating conditions and stringent autonomy requirements, pose important design challenges to make them provide automated analysis for complex biological signals. This talk addresses ultra-low power design of next-generation smart WBSN platforms for multimodal bio-signal monitoring systems, and highlights the unsustainable energy cost incurred by the relatively straightforward wireless streaming of raw sensor data. To achieve the extended autonomy required by long-term ambulatory monitoring, this talk advocates for enabling more embedded intelligence onboard these sensor nodes through a new system-level design approach. This approach exploits the bio-signal features to apply the new compressive sensing paradigm in the design of specialized near-threshold computing and memory blocks in order to deploy ultra-low power (ULP) multi-core processing architectures for automated bio-signals analysis on WBSN. To illustrate the effectiveness of this approach, this talk focuses on cardiac monitoring systems and show how it is possible to achieve multi-modal wearable systems based on wearable ULP electrocardiogram (ECG) arrhythmia detection systems that can operate autonomously for long periods of time and support a graceful quality degradation of the system output based on the available power.
(slides)

With the rise of sensors such as the Microsoft Kinect, Leap Motion, and hand motion sensors in phones (i.e., Samsung Galaxy S5), gesture-based interfaces have become practical. Unfortunately, today, to recognize such gestures, applications must have access to depth and video of the user, exposing sensitive data about the user and her environment. Besides these privacy concerns, there are also security threats in sensor-based applications, such as multiple applications registering the same gesture, leading to a conflict (akin to Clickjacking on the web).

We address these security and privacy threats with PrePose, a novel domain-specific language (DSL) for easily building gesture recognizers, combined with a system architecture that protects user privacy against untrusted applications. We run PrePose code in a trusted core, and only return specific gesture events to applications. PrePose is specifically designed to enable precise and sound static analysis using SMT solvers, allowing the system to check security and privacy properties before running a gesture recognizer. We demonstrate that PrePose is expressive by creating a total of 28 gestures in three representative domains: physical therapy, tai-chi, and ballet. We further show that runtime gesture matching in PrePose is fast, creating no noticeable lag, by measuring on traces obtained from Microsoft Kinect runs.

To show that gesture checking at the time of submission to a gesture store is fast, we developed a total of four Z3-based static analyses to test for basic gesture safety and internal validity, to make sure the so-called protected gestures are not overridden, and to check inter-gesture conflicts. Our static analysis scales well in practice: safety checking is under 0.5 seconds per gesture; average validity checking time is only 188 ms; lastly, for 97% of the cases, the conflict detection time is below 5 seconds, with only one query taking longer than 15 seconds.

Unification is a core component of every proof assistant or programming language featuring dependent types. In many cases, it must deal with higher-order problems up to conversion. Since unification in such conditions is undecidable, unification algorithms may include several heuristics to solve common problems. However, when the stack of heuristics grows large, the result and complexity of the algorithm can become unpredictable.

Our contributions are twofold: (1) We present a full description of a new unification algorithm for the Calculus of Inductive Constructions (the base logic of Coq), including universe polymorphism, canonical structures (the overloading mechanism baked into Coq's unification), and a small set of useful heuristics. (2) We implemented our algorithm, and tested it on several libraries, providing evidence that the selected set of heuristics suffices for large developments.

M-Goup focus is in empirical software engineering in software and data intensive systems and services. It is a research group increasing rapidly its academic competence and achievements. This is demonstrated e.g. by growing number of publications, PhD theses and two FiDiPro professors.

M-Group has four full professors, two FiDiPro professors, six post-doc researchers and over 40 PhD students. The research of the group has been rated as excellent (5/6) in an international external RAE evaluation.

We carry out research typically in collaboration with industry. A wide domestic and international industrial contact network provides a solid basis for empirical research that has high quality academic impact and also strong relevance for practitioners. Our Cloud Software Factory and the related ecosystem with companies and other Software Factories provides an environment in which we can carry out student experiments as well as industrial experiments and case studies.

M-Group has a long tradition in international collaboration. The group is a member of ISERN (Prof. Oivo one of its six founding members) and has actively participated in large European research projects since the 1990's. Our personnel are very international and we are happy to host both long and short term visitors. The everyday working language and documentation is English which makes it easy for members to adjust within the group.

The main topics of empirical research for software and data intensive systems and services include:

• Processes and quality
• Agile & Lean methods
• Software development methodologies
• Requirements engineering
• Software and system architectures
• Testing
• Cloud based development and systems (in and for cloud)
• Service design methods and tools
• Data science
• Privacy & Security

A great deal of effort has been spent on both trying to specify software requirements and on ensuring that software actually matches these requirements. A wide range of techniques that includes theorem proving, model checking, type-based analysis, static analysis, runtime monitoring, and the like have been proposed. However, in many areas adoption of these techniques remains spotty. In fact, obtaining a specification or a precise notion of correctness is in many cases quite elusive. For many programming tasks, even expert developers are unable to get them right because of numerous tricky corner cases.

In this paper we investigate an approach we call program boosting, which involves crowd-sourcing partially correct solutions to a tricky programming problem from developers and then blending these programs together in a way that improves correctness.

We show how interesting and highly non-trivial programming tasks such as writing regular expressions to match URLs and email addresses can be effectively crowd-sourced. We demonstrate that carefully blending the crowd-sourced results together frequently yields results that are better than any of the individual responses. Our experiments on 465 of programs show consistent boosts in accuracy and demonstrate that program boosting can be performed at a relatively modest monetary cost.

Automated test generation for object-oriented software typically consists of producing sequences of calls aiming at high code coverage. In practice, the success of this process may be inhibited when classes interact with their environment, such as the file system, network, user-interactions, etc. This leads to two major problems: First, code that depends on the environment can sometimes not be fully covered simply by generating sequences of calls to a class under test, for example when execution of a branch depends on the contents of a file. Second, even if code that is environment- dependent can be covered, the resulting tests may be unstable, i.e., they would pass when first generated, but then may fail when executed in a different environment. For example, tests on classes that make use of the system time may have failing assertions if the tests are executed at a different time than when they were generated.

In this talk, we present an approach that applies bytecode instrumentation to automatically separate code from its environmental dependencies, and extend the EVOSUITE Java test generation tool such that it can explicitly set the state of the environment as part of the sequences of calls it generates. Using a prototype implementation, which handles a wide range of environmental interactions such as the file system, console inputs and many non-deterministicfunctions of the Java virtual machine (JVM), we performed experiments on 100 Java projects randomly selected from SourceForge (the SF100 corpus). The results show significantly improved code coverage -- in some cases even in the order of +80%/+90%. Furthermore, our techniques reduce the number of unstable tests by more than 50%.