Existing software model checkers based on predicate abstraction and refinement typically perform poorly at verifying the absence of buffer overflows, with analyses depending on the sizes of the arrays checked. We observe that many of these analyses can be made efficient by providing proof templates for common array traversal idioms idioms, which guide the model checker towards proofs that are independent of array size. We have integrated this technique into our software model checker, PtYasm, and have evaluated our approach on a set of testcases derived from the Verisec suite, demonstrating that our technique enables verification of the safety of array accesses independently of array size.

We describe PTYASM, an enhanced version of the YASM software model checker which uses proof templates. These templates associate correctness arguments with common programming idioms, thus enabling efficient verification. We have used PTYASM to verify the safety of array accesses in programs derived from the Verisec suite. PTYASM is able to verify this property in the majority of testcases, while existing software model checkers fail to do so due to loop unrolling.

Software model checking based on abstraction-refinement has recently achieved widespread success in verifying API conformance in device drivers, and we believe this success can be replicated for the problem of buffer overflow detection. This paper presents a publicly-available benchmark suite to help guide and evaluate this research. The benchmark consists of 298 code fragments of varying complexity capturing 22 buffer overflow vulnerabilities in 12 open source applications. We give a preliminary evaluation of the benchmark using the SatAbs model checker

Achieving high performance for concurrent applications on modern multiprocessors remains challenging. Many programmers avoid locking to improve performance, while others replace locks with non-blocking synchronization to protect against deadlock, priority inversion, and convoying. In both cases, dynamic data structures that avoid locking, require a memory reclamation scheme that reclaims nodes once they are no longer in use. The performance of existing memory reclamation schemes has not been thoroughly evaluated. We conduct the first fair and comprehensive comparison of three recent schemes -quiescent-state-based reclamation, epoch-based reclamation, and hazard-pointer-based reclamation - using a flexible microbenchmark. Our results show that there is no globally optimal scheme. When evaluating lockless synchronization, programmers and algorithm designers should thus carefully consider the data structure, the workload, and the execution environment, each of which can dramatically affect memory reclamation performance

We evaluate the robustness of simplified mobility and radio propagation models for indoor MANET simulations. A robust simplification allows researchers to extrapolate simulation results and reach reliable conclusions about the expected performance of protocols in real life. We show that common simplified mobility and radio propagation models are not robust. Experiments with DSR and DSDV, two representative MANET routing protocols, show that the simplifications affect the two protocols in very different manners. Even for a single protocol, the effects on perceived performance can vary erratically as parameters change. These results cast doubt on the soundness of evaluations of MANET routing protocols based on simplified mobility and radio propagation models, and expose the urgent need for more research on realistic MANET simulation.