ABSTRACT
Introduction Property-based testing is a technique for testing the security of programs. Recall that secure means conforming to a security policy. e analyst doing the testing
rst species the properties she wishes the program to conform to. e program is then instrumented based on the specication of the properties. Consider the execution of the program as a state machine, where as each instruction is executed, the state of the program changes. Relevant changes aect only those portions of the state used in the properties. e instrumentation produces output whenever such a change occurs. e program is then executed under control of another program called the test execution monitor (TEM). e TEM is given the properties, and whenever the execution enters a state forbidden by the specied by the properties, it reports a security error.
