Towards a Property-based Testing Environment with Applications

We consider an approach to testing that combines white-box and black-box techniques. Black-box testing is used for testing a program's effects against its specification. White-boxtesting is essential if subtle implementation errors are to be identified, 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 substantially simplify much of the testing work. The portion of a program that relates to a given property can be identified through slicing. Wedescribe the ongoing developmentofaTester's Assistant, which in the long term, will include a specification-driven slicer for C programs, a test data generator, a coverage analyzer, and an execution monitor. The slicer and execution monitor are described in this paper, and applications to Unix security are indicated. Securityisanimportant application of property-based testing because of the subtle undetected security errors in delivered operating systems. It is also a promising application because of the (unexpectedly) concise specifications that capture most security requirements, and because of the operating system support for execution monitoring