#	Pagina
attuale pagina	/open-h2020/projects/194494/results.html
-1	/open-h2020/per-topic/3b/list/index.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - SYMBIOSYS (Symbolic Analysis of Temporal and Functional Behavior of Networked Systems)

Teaser

Summary

The goal of SYMBIOSYS is to achieve reliability and interoperability of networked (software) systems, a crucial requirement in todayâ€™s networked information society. To this end, we devise a software and systems analysis methodology that â€“ for the first time â€“ considers the vital influence factors that determine the behavior of networked systems, especially including input and temporal uncertainty of network interactions. With SYMBIOSYS, we want be able to automatically and efficiently explore and analyze the vast amount of distributed execution paths in networked systems in a highly structured manner inspired by Symbolic Execution (SE).
The combination of the benefits of model checking (rigorous exploration) and of dynamic software testing (analyzing real systemsâ€™ code) represents a quantum leap in the field of networked systems analysis. Orthogonal to and complementing formal model-based approaches, which target the design of reliable systems on an abstract (model-) level, we also address system- and implementation-level aspects of (typically heterogeneous) implementations that interact via unpredictable networks. To achieve this, we introduce the fundamentally new approaches Symbolic Distributed Execution (SDE), Symbolic Temporal Execution (STE) and their symbiosis (SDTE). This is a breakthrough in the symbolic analysis of real systems and significantly widens the scope of SE to new analysis domains.

Work performed

As the primary challenges of the SYMBIOSYS project lie not so much in implementing a working prototype of the Symbolic Distributed Temporal Execution (SDTE) approach, but rather in doing so in a manner that is performant and capable enough to enable the analysis of anything more than the most trivial of examples, we have bent our primary focus on the performance of four different key areas:
1. As Symbolic Execution as well as the proposed SDTE are based on Satisfiability Modulo Theories (SMT) constraint solvers, we have evaluated possible improvements. We have especially looked at the integration points where Symbolic Execution comes into contact with the SMT solver, as our main competences are found in Symbolic Execution rather than core SMT solving research. While our successes in this area have not been published in the period covered by this report, results are currently under peer-review which are based upon the work performed therein. In fact, we have also presented additional advances during the 1st International KLEE Workshop on Symbolic Execution, which took place shortly after the end of the period reviewed in this report.
2. Performance of the discrete event simulation that will be integrated with the Symbolic Distributed Execution to perform temporal advances. Our current prototype has benefitted from our venues in this area, as we became able to develop a very fine-grained modularization, which in turn enables the SDE component to defer any forks for as long as possible, and even eschew them as much as possible. We are proud to say that our published contributions in this area have won multiple awards.
3. Advances in the basic Symbolic Execution technology underlying SDTE. These advances are in fact twofold: Firstly, we performed work on improving the performance of the Symbolic Execution engine itself. Again, by improving the performance in parts of the engine that are especially exercised by SDTE, we can create a basis that is able to support SDTE to a greater degree than would be possible without. For example, we have worked on the support of state merging, a technique to reduce path explosion, in the KLEE Symbolic Execution engine that our SDTE prototype is built upon. Secondly, we have considered which features are missing from contemporary Symbolic Execution engines, and have, e.g., published an award-winning paper that discusses providing floating-point number support for Symbolic Execution.
Another problem of Symbolic Execution that becomes especially important with the extension to networked systems (SDE) is that of infinite loops. As Symbolic Execution is a dynamic analysis, its computational complexity depends on the program under test, which causes infinite loops in the target program â€“ such as those commonly occurring in servers â€“ to also have infinite analysis time. We worked on a technique that enables us to detect violations of program liveness with Symbolic Execution or SDE. This work was accepted to one of the premier conferences in the area of software engineering, verification and testing, the 30th International Conference on Computer Aided Verification (CAVâ€™18).
4. While this first period has necessarily begun by exploring and improving the foundation of our work, we have of course also worked on our SDTE technique. We have made significant advances at integrating STE into our SDE prototype. As of the end of scientific period one, we can analyze (still very simple) distributed programs. We were able to integrate the two techniques in a manner that leaves us hopeful to achieve the necessary performance to analyze real-world programs by the end of the SYMBIOSYS project.