Towards a Property-Based Testing Environment With Applications to Security-Critical Software
CALIFORNIA UNIV DAVIS DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
We consider an approach to testing that combines white-box and black-box techniques. Black-box testing is used for testing a programs effects against its specification. White-box testing 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. We describe the ongoing development of a Testers Assistant, which in the long term, will include a specification-driven slicer for C programs, a test data generator, a coverage analyzer, an execution monitor. The slicer and execution monitor are described in this paper, and applications to Unix security are indicated. Security is an important 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.
- Computer Programming and Software
- Computer Systems Management and Standards