Program logics are formal logics designed to facilitate specification and correctness reasoning for software programs. Separation logic, a recent program logic for C-like programs, has found great success in automated verification due in large part to its embodiment of the principle of local reasoning, in which specifications and proofs are restricted to just those resources—variables, shared memory addresses, locks, etc.—used by the program during execution. Existing program logics make the strong assumption that all threads agree on the values of shared memory at all times. But, on modern computer architectures, this assumption is unsound for certain shared-memory concurrent programs: namely, those with races. Typically races are considered to be errors, but some programs, like lock-free concurrent data structures, are necessarily racy. Verification of these difficult programs must take into account the weaker models of memory provided by the architectures on which they execute. This dissertation project seeks to explicate a local reasoning principle for x86-like architectures. The principle is demonstrated with a new program logic for concurrent C-like programs that incorporates ideas from separation logic. The goal of the logic is to allow verification of racy programs like concurrent data structures for which no general-purpose high-level verification techniques exist. / text

Not available

In safety-critical real-time embedded systems, correctness is of primary concern, as even small transient errors may lead to catastrophic consequences. Due to the limitations of well-established methods such as verification and testing, recently runtime verification has emerged as a complementary approach, where a monitor inspects the system to evaluate the specifications at run time. The goal of runtime verification is to monitor the behavior of a system to check its conformance to a set of desirable logical properties. The literature of runtime verification mostly focuses on event-triggered solutions, where a monitor is invoked when a significant event occurs (e.g., change in the value of some variable used by the properties). At invocation, the monitor evaluates the set of properties of the system that are affected by the occurrence of the event. This type of monitor invocation has two main runtime characteristics: (1) jittery runtime overhead, and (2) unpredictable monitor invocations. These characteristics result in transient overload situations and over-provisioning of resources in real-time embedded systems and hence, may result in catastrophic outcomes in safety-critical systems. To circumvent the aforementioned defects in runtime verification, this dissertation introduces a novel time-triggered monitoring approach, where the monitor takes samples from the system with a constant frequency, in order to analyze the system's health. We describe the formal semantics of time-triggered monitoring and discuss how to optimize the sampling period using minimum auxiliary memory and path prediction techniques. Experiments on real-time embedded systems show that our approach introduces bounded overhead, predictable monitoring, less over-provisioning, and effectively reduces the involvement of the monitor at run time by using negligible auxiliary memory. We further advance our time-triggered monitor to component-based multi-core embedded systems by establishing an optimization technique that provides the invocation frequency of the monitors and the mapping of components to cores to minimize monitoring overhead. Lastly, we present RiTHM, a fully automated and open source tool which provides time-triggered runtime verification specifically for real-time embedded systems developed in C.

Information flow security concerns how to protect sensitive data in computer systems by avoiding undesirable flow of information between the users of the systems. This thesis studies information flow security properties in state-based systems, dealing in particular with modelling and verification methods for asynchronous systems and synchronous systems with schedulers. The aim of this study is to provide a foundational guide to ensure confidentiality in system design and verification. The thesis begins with a study of definitions of security properties in asynchronous models. Two classes of security notions are of particular interest. Trace-based properties disallow deductions of high security level secrets from low level observation traces. Bisimulation-based properties express security as a low-level observational equivalence relation on states. In the literature, several distinct schools have developed frameworks for information flow security properties based on different semantic domains. One of the major contributions of the thesis is a systematic study that compares security notions, using semantic mappings between two state-based models and a particular process algebraic model. An advantage of state-based models is the availability of well-developed verification methods and tools for functional properties in finite state systems. The thesis investigates the application of these methods to the algorithmic verification of the information flow security properties in the asynchronous settings. The complexity bounds for verifying these security properties are given as polynomial time for the bisimulation-based properties and polynomial space complete for the trace-based properties. Two heuristics are presented to benefit the verifications of the properties in practice. Timing channels are one of the major concerns in the computer security community, but are not captured in asynchronous models. In the final part of the thesis, a new system model is defined that deals with timing and scheduling. A group of novel security notions, including both trace-based and bisimulation-based properties, are proposed in this new model. It is further investigated whether these security properties are preserved by refinement of schedulers and scheduler implementations. A case study of a multi- evel secure file server is described, which applies a number of access control rules to enforce a particular bisimulation-based property in the synchronous setting.

The field of chip design is characterized by contradictory pressures to reduce time-to-market and maintain a high level of reliability. As a result, module reuse has become common practice in chip design. To save time on both design and verification, Systems-on-Chips (SoCs) are composed using pre-designed and pre-verified modules. The integrated modules are often designed by different groups and for different purposes, and are later integrated into a single chip. In the absence of a single interface standard for such modules, "plug-n-play" style integration is not likely, as the subject modules are often designed to comply with different interface protocols. For such modules to communicate correctly there is a need for some glue logic, also called a protocol converter that mediates between them. Though much research has been dedicated to the protocol converter synthesis problem of SoC communication, converter synthesis is still performed manually, consuming development and verification time and risking human error. Current approaches to automatic synthesis of protocol converters mostly lack formal foundations and either employ abstractions far removed from the Hardware Description Language (HDL) implementation level or grossly simplify the structure of the protocols considered. This thesis develops and presents techniques for automatic synthesis of provably correct on-chip protocol converters. Basing the solution on a formal approach, a novel state-machine based formalism is presented for modelling bus-based protocols and formalizing the notions of protocol compatibility and correct protocol conversion. Algorithms for automatic compatibility checking and provably-correct converter synthesis are derived from the formalism, including a systematic exploration of the design space of the protocol converter, the first in the field, which enables generation of various alternative deterministic converters. The work presented is unique in its combination of a completely formal approach and the use of a low abstraction level that enables precise modelling of protocol characteristics and automatic translation of the constructed converter to HDL.

The field of chip design is characterized by contradictory pressures to reduce time-to-market and maintain a high level of reliability. As a result, module reuse has become common practice in chip design. To save time on both design and verification, Systems-on-Chips (SoCs) are composed using pre-designed and pre-verified modules. The integrated modules are often designed by different groups and for different purposes, and are later integrated into a single chip. In the absence of a single interface standard for such modules, "plug-n-play" style integration is not likely, as the subject modules are often designed to comply with different interface protocols. For such modules to communicate correctly there is a need for some glue logic, also called a protocol converter that mediates between them. Though much research has been dedicated to the protocol converter synthesis problem of SoC communication, converter synthesis is still performed manually, consuming development and verification time and risking human error. Current approaches to automatic synthesis of protocol converters mostly lack formal foundations and either employ abstractions far removed from the Hardware Description Language (HDL) implementation level or grossly simplify the structure of the protocols considered. This thesis develops and presents techniques for automatic synthesis of provably correct on-chip protocol converters. Basing the solution on a formal approach, a novel state-machine based formalism is presented for modelling bus-based protocols and formalizing the notions of protocol compatibility and correct protocol conversion. Algorithms for automatic compatibility checking and provably-correct converter synthesis are derived from the formalism, including a systematic exploration of the design space of the protocol converter, the first in the field, which enables generation of various alternative deterministic converters. The work presented is unique in its combination of a completely formal approach and the use of a low abstraction level that enables precise modelling of protocol characteristics and automatic translation of the constructed converter to HDL.

This thesis examines applying formal methods to software testing. Software testing is a critical phase of the software life-cycle which can be very effective if performed rigorously. Formal specifications offer the bases for rigorous testing practices. Not surprisingly, the most immediate use of formal specifications in software testing is as sources of black-box test suites. However, formal specifications have more uses in software testing than merely being sources for test data. We examine these uses, and show how to get more assistance and benefit from formal methods in software testing. At the core of this work is a exible framework in which to conduct specification-based testing. The framework is founded on formal definitions of tests and test suites, which directly addresses important issues in managing software testing. This provides a uniform platform for other applications of formal methods to testing such as analysis and reification of tests, and also for applications beyond testing such as maintenance and specification validation. The framework has to be exible so that any testing strategies can be used. We examine the need to adapt certain strategies to work with the framework and formal specification. Our experiments showed some deficiencies that arise when using derivation strategies on abstract specifications. These deficiencies led us to develop two new specification-based testing strategies based on extensions to existing strate- gies. We demonstrate the framework, strategies, and other applications of formal methods to software testing using three case studies. In each of these, the framework was easy to use. It provided an elegant and powerful means for defining and structuring tests, and a suitable staging ground for other applications of formal methods to software testing. This thesis demonstrates how formal specification techniques can systematise the application of testing strategies, and also how the concepts of software testing can be combined with formal specifications to extend the role of the formal specification in software development.

This thesis presents an approach to reusing components which alleviates some of the main problems encountered in component-based reuse; in particular modifying components to suit user's specific needs, and locating suitable components within a library. The focus of the thesis is on components described using a formal language (in other words components with a formal interface specification). The main reason for this is the concise and precise nature of formal languages, which can be exploited in developing more sophisticated methods and tools which take advantage of the semantics of the component. The solution is presented in two main stages: firstly a framework for adapting components is defined; secondly a framework for retrieving components based on matching component interfaces is defined. Both of these frameworks take advantage of the formal nature of the component interfaces, as a result more sophisticated tools can be developed. For generality it is proposed that formal languages used to represent interfaces are partitioned into three separate levels of granularity - expressions, units and modules - and solutions to adaptation and retrieval are developed separately at each level. An important consideration in developing these frameworks is to ensure that certain component properties are preserved when adapting and retrieving components. Having proposed these general frameworks, algorithms for adapting and retrieving components are defined in a more concrete and detailed sense within the CARE system. CARE was chosen because the language is relatively simple and compact, yet contains many of the features found in other formal languages, including: variables; functions; predicates; binders; application; typing; parameters; inputs and outputs (and their types); preconditions and postconditions; textual and formal parameters; separation of specification and implementation; case statements; modules; applicability conditions; encapsulation; and information hiding. These techniques for adapting and retrieving components have been prototyped as extensions to existing CARE tools. As a means of illustrating the value that these extensions have added to the overall CARE system, several example developments using the extended tools are presented at the end of the thesis. The approach to component reuse presented in this thesis represents a significant advance on other similar approaches. The approach given here is far more general than other approaches, particularly with respect to the scope of components and their interfaces that are considered. Also the adaptation framework goes beyond other approaches which have typically been restricted to parameter instantiation.

Diss. Uppsala : Univ., 2005.

Diss. Uppsala : Uppsala universitet, 2005.