The goal of SYMBIOSYS is to assure the 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 will 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 network 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 significantly widens the scope of Symbolic Execution to new analysis domains. 

Bugs Discovered

• Non-termination bug in tail (GNU Coreutils) - Bug Report
• Non-termination bug #2 in tail (GNU Coreutils) - Bug Report
• Non-termination bug in ptx (GNU Coreutils) - Bug Report
• Non-termination bug in hush (BusyBox) - Bug Report
• Non-termination bug #2 in hush (BusyBox) - Bug Report
• Non-termination bug in GNU regex - Bug Report
• Segfault in z3 - Bug Report
• Unsafe usage of non-volatile object in a signal handler in GNU gzip - Bug Report
• Use-after-free in QUANT - Bug Report
• QUIC stream not correctly closed in QUANT - Bug Report
• Segfault in LLVM - Bug Report
• 6 double-initialized mutexes in memcached - Bug Report
• Data race in memcached - Bug Report
• Data race #2 in memcached - Bug Report
• Data race #3 in memcached - Bug Report
• Regression in out-of-memory situations in jq - Bug Report
• Illegal null-pointer argument in jtc - Bug Report
• Use-after-free in jtc - Bug Report
• Out-of-bounds error during string parsing in jtc - Bug Report
• Heap use-after-free in jq - Bug Report
• Segfault in toybox sed - Bug Report

Awards

• Best Paper Award: Automated Memoization for Parameter Studies Implemented in Impure Languages (SIGSIM-PADS’16)
• Best Experience Paper Award: Floating-Point Symbolic Execution: A Case Study in N-Version Programming (ASE'17)
• Computing Reviews - Included in the Notable Books and Articles in Computing of 2016: Automated Memoization for Parameter Studies Implemented in Impure Languages

Team

Contact

For questions and inquiries regarding the SYMBIOSYS project, please contact:

   Daniel Schemmel
   Systems Analysis Group

   E-Mail: daniel.schemmel at comsys.rwth-aachen.de
   Phone: +49 241 80-21420

Funding

This research is supported by the European Research Council (ERC) under the EU’s Horizon 2020 Research and Innovation Programme (grant agreement n. 647295 (SYMBIOSYS)).