Kaled M. Alshmrany

Kaled M. Alshmrany, Mohannad Aldughaim, Ahmed Bhayat et al.

FuSeBMC is a test generator for finding security vulnerabilities in C programs. In earlier work [4], we described a previous version that incrementally injected labels to guide Bounded Model Checking (BMC) and Evolutionary Fuzzing engines to produce test cases for code coverage and bug finding. This paper introduces a new version of FuSeBMC that utilizes both engines to produce smart seeds. First, the engines are run with a short time limit on a lightly instrumented version of the program to produce the seeds. The BMC engine is particularly useful in producing seeds that can pass through complex mathematical guards. Then, FuSeBMC runs its engines with more extended time limits using the smart seeds created in the previous round. FuSeBMC manages this process in two main ways using its Tracer subsystem. Firstly, it uses shared memory to record the labels covered by each test case. Secondly, it evaluates test cases, and those of high impact are turned into seeds for subsequent test fuzzing. As a result, we significantly increased our code coverage score from last year, outperforming all tools that participated in this year's competition in every single category.

Mohannad Aldughaim, Kaled Alshmrany, Rafael Menezes et al.

Bounded model checking (BMC) is vital for finding program property violations. For unsafe programs, BMC can quickly find an execution path from an initial state to the violated state that refutes a given safety property. However, BMC techniques struggle to falsify programs that contain loops. BMC needs to incrementally unfold the program loops up to the bound $k$, exposing the property violation, which can thus lead to exploring a considerable state space. Here, we describe and evaluate the first verification method based on interval methods via contractors to reduce the domains of variables representing the search space. This reduction is based on the specified property modeled as functions representing the contractor constraints. In particular, we exploit interval methods via contractors to incrementally analyze the program loop variables and contract the domain where the property is guaranteed to hold to prune the search exploration, thus reducing resource consumption aggressively. Experimental results demonstrate the efficiency and efficacy of our proposed approach over a large set of benchmarks, including $7044$ verification tasks, compared with state-of-the-art BMC tools. Our proposed method can reduce memory usage up to $75$\% while verifying $1$\% more verification tasks.

Kaled M. Alshmrany, Rafael S. Menezes, Mikhail R. Gadelha et al.

We describe and evaluate a novel white-box fuzzer for C programs named FuSeBMC, which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. FuSeBMC explores and analyzes C programs (1) to find execution paths that lead to property violations and (2) to incrementally inject labels to guide the fuzzer and the BMC engine to produce test-cases for code coverage. FuSeBMC successfully participates in Test-Comp'21 and achieves first place in the Cover-Error category and second place in the Overall category.

Kaled Alshmrany, Lucas Cordeiro

Implementations of network protocols are often prone to vulnerabilities caused by developers' mistakes when accessing memory regions and dealing with arithmetic operations. Finding practical approaches for checking the security of network protocol implementations has proven to be a challenging problem. The main reason is that the protocol software state-space is too large to be explored. Here we propose a novel verification approach that combines fuzzing with symbolic execution to verify intricate properties in network protocol implementations. We use fuzzing for an initial exploration of the network protocol, while symbolic execution explores both the program paths and protocol states, which were uncovered by fuzzing. From this combination, we automatically generate high-coverage test input packets for a network protocol implementation. We surveyed various approaches based on fuzzing and symbolic execution to understand how these techniques can be effectively combined and then choose a suitable tool to develop further our model on top of it. In our preliminary evaluation, we used ESBMC, Map2Check, and KLEE as software verifiers and SPIKE as fuzzer to check their suitability to verify our network protocol implementations. Our experimental results show that ESBMC can be further developed within our verification framework called \textit{FuSeBMC}, to efficiently and effectively detect intricate security vulnerabilities in network protocol implementations.