English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Finding software vulnerabilities in concurrent programs is a challenging taskdue to the size of the state-space exploration, as the number of interleavingsgrows exponentially with the number of program threads and statements. Wepropose and evaluate EBF (Ensembles of Bounded Model Checking with Fuzzing) --a technique that combines Bounded Model Checking (BMC) and Gray-Box Fuzzing(GBF) to find software vulnerabilities in concurrent programs. Since there areno publicly-available GBF tools for concurrent code, we first propose OpenGBF-- a new open-source concurrency-aware gray-box fuzzer that explores differentthread schedules by instrumenting the code under test with random delays. Then,we build an ensemble of a BMC tool and OpenGBF in the following way. On the onehand, when the BMC tool in the ensemble returns a counterexample, we use it asa seed for OpenGBF, thus increasing the likelihood of executing paths guardedby complex mathematical expressions. On the other hand, we aggregate theoutcomes of the BMC and GBF tools in the ensemble using a decision matrix, thusimproving the accuracy of EBF. We evaluate EBF against state-of-the-art pureBMC tools and show that it can generate up to 14.9% more correct verificationwitnesses than the corresponding BMC tools alone. Furthermore, we demonstratethe efficacy of OpenGBF, by showing that it can find 24.2% of thevulnerabilities in our evaluation suite, while non-concurrency-aware GBF toolscan only find 0.55%. Finally, thanks to our concurrency-aware OpenGBF, EBFdetects a data race in the open-source wolfMqtt library and reproduces knownbugs in several other real-world programs, which demonstrates its effectivenessin finding vulnerabilities in real-world software.

Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs