Toward a Property-based Testing Environment with Application to Security Critical Software

We consider an approach to testing that combines white-box and black-box techniques. Black-box testing is used for testing a program's eects against its specication. White-box test-ing is essential if subtle implementation errors are to be identied, e.g., errors due to race conditions. Full white-box testing is a large task. However, for many properties, only a small portion of the program is relevant | hence property-based testing has the potential to sub-stantially simplify much of the testing work. The portion of a program that relates to a given prop-erty can be identied through slicing. We de-scribe the ongoing development of a Tester's As-sistant, which in the long term, will include a speci cation-driven slicer for C programs, a test data generator, a coverage analyzer, and an exe-cution monitor. The slicer and execution moni-tor are described in this paper, and applications to Unix security are indicated. Security is an im-portant application of property-based testing be-cause of the subtle undetected security errors in delivered operating systems. It is also a promis-ing application because of the (unexpectedly) concise specications that capture most security requirements, and because of the operating sys-tem support for execution monitoring. The work reported here is being supported in part by ARPA under contract USNN00014-94-1-0065 and by the Lawrence Livermore National Laboratory under work order LLNL-IUTB234584