Software model checking as well as runtime verification are verification techniques which are widely used for checking temporal properties of software systems. Even though they are property ...verification techniques, their common usage in practice is in "bug finding", that is, finding violations of temporal properties. Motivated by this observation and leveraging the recent progress in fuzzing, we build a greybox fuzzing framework to find violations of Linear-time Temporal Logic (LTL) properties. Our framework takes as input a sequential program written in C/C++, and an LTL property. It finds violations, or counterexample traces, of the LTL property in stateful software systems; however, it does not achieve verification. Our work substantially extends directed greybox fuzzing to witness arbitrarily complex event or-derings. We note that existing directed greybox fuzzing approaches are limited to witnessing reaching a location or witnessing simple event orderings like use-after-free. At the same time, compared to model checkers, our approach finds the counterexamples faster, thereby finding more counterexamples within a given time budget. Our LTL-FUZZER tool, built on top of the AFL fuzzer, is shown to be effective in detecting bugs in well-known protocol implementations, such as OpenSSL and Telnet. We use LTL-FUZZER to reproduce known vulnerabilities (CVEs), to find 15 zero-day bugs by checking properties extracted from RFCs (for which 12 CVEs have been assigned), and to find violations of both safety as well as liveness properties in real-world protocol implementations. Our work represents a practical advance over software model checkers - while simultaneously representing a conceptual advance over existing greybox fuzzers. Our work thus provides a starting point for understanding the unexplored synergies among software model checking, runtime verification and greybox fuzzing.
CoVeriTeam Service: Verification as a Service Beyer, Dirk; Kanav, Sudeep; Wachowitz, Henrik
2023 IEEE/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)
Conference Proceeding
Odprti dostop
The research community has developed numerous tools for solving verification problems, but we are missing a common web interface for executing them. This means, users have to commit to install and ...execute each new tool (version) on their local machine. We propose to use Coveriteam Service to make it easy for verification researchers to experiment with new verification tools. CoVeriteam has already unified the command-line interface, and reduced the burden by taking care of tool installation and isolated execution. The new web service in addition enables tool developers to make their tools accessible on the web and users to include verification tools in their work flow. There are already further applications of our service: The 2023 competitions on software verification and testing used the service for their integration testing, and we propose to use Coveriteam Service for incremental verification as part of a continuous-integration process. Demonstration video: https://youtu.be/0Ao0ZogSu1U Demonstration service: https://coveriteam-service.sosy-lab.org
This book discusses the historical networking environment that gave rise to SDN, as well as the latest advances in SDN technology. It provides state of the art knowledge needed for successful ...deployment of an SDN, including how to explain to the non-technical business decision makers in an organization the potential benefits and risks, in shifting parts of a network to the SDN model; how to make intelligent decisions about when to integrate SDN technologies in a network; how to decide if an organization should be developing its own SDN applications or looking to acquire them from an outside vendor; how to accelerate the ability to develop an SDN application; discusses the evolution of the switch platforms that enable SDN; addresses when to integrate SDN technologies in a network; provides an overview of sample SDN applications relevant to different industries; includes practical examples of how to write SDN applications. --
PDF
