Talk: Property Checking by Combining Verification and Testing
Software validation is the task of determining if the software meets the expectations of its users. For the most part, industrial practice of software engineering uses testing to validate software. Testing is incomplete in the sense that it validates the software only for the test inputs that we execute. The software might exhibit undesired behavior with test inputs we do not have. The holy grail of software validation is verification. Here, the goal is to formally prove that the software meets its expectations for all possible test inputs, and for all possible executions.
In practice, verification efforts run into two major difficulties. First, it is very hard to formally specify expectations as specifications in a formal language that can be input to a verification tool. Complete specifications of complex software (like an operating system) could be as complex as the software itself, and it is very hard to get programmers and system designers to write specifications. Next, even if specifications were to somehow exist, the scale and complexity of large software (which can run into tens of millions of lines of source code) is well beyond the capabilities of today's verification tools.
In this short paper, we discuss some possible approaches for these problems. First, in order to the address the difficulties in writing specifications, we believe that there are ways by which we can ask programmers for high-level guidelines about the structure of specifications, and use statistical techniques to automatically generate detailed specifications. Second, in order to address scalability, we believe that we can exploit the continuum between verification and testing, and design hybrid algorithms that combine testing and verification.
Talk: Security Testing and Formal Methods for High Levels Certification of Smart Cards
We will discuss security testing and formal methods in the framework of the Common Criteria certification of smart cards. The discussion will introduce the requirements of the standard on the test activity and on the description of the design and will identify their impact on the methods and tools to use. Emphasis will be placed on the high levels of certification in which formal methods are required to demonstrate the correct design of the security. We will discuss the advantage of a mixed approach of formal model-based testing, that will allow to reach, in a pragmatic way, high levels of certification.