Towards a Property-Based Testing Environment With Applications to Security-Critical Software
Abstract
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-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 Tester's 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1994
- Accession Number
- ADA445720
Entities
People
- Calvin Ko
- George Fink
- Karl Levitt
- Myla Archer
Organizations
- University of California, Davis