A biform theory is a combination of an axiomatic theory and an algorithmic theory. It is used to integrate reasoning and computation in a common theory and can include algorithms with precisely specified input-output relationships. Isabelle is one of the leading interactive theorem provers. Isabelle includes locales, a module system that uses theory morphisms to manage theory hierarchies, and that has a rich and extensive library with multiple useful proof and formalization techniques. A case study of eight biform theories of natural number arithmetic is described in the paper “Formalizing Mathematical Knowledge as a Biform Theory Graph” by J. Carette and W. M. Farmer. The biform theories form a graph linked by theory morphisms. Seven of the biform theories are in first-order logic and one is in simple type theory. The purpose of this thesis is to test how a theory graph of biform theories can be formalized in Isabelle by attempting to formalize this case study. We work with locales and sublocales in Isabelle to formalize the test case. The eight biform theories are defined as regular axiomatic theories, while the algorithms are functions defined on inductive types representing the syntax of the theories. / Thesis / Master of Science (MSc)

No description available.

No description available.

No description available.

No description available.

Template semantics is a template-based approach to describing the semantics of model-based notations, where a pre-defined template captures the notations' common semantics, and parameters specify the notations' distinct semantics. In this thesis, we investigate using template semantics to parameterize the translation from a model-based notation to the input language of the SMV family of model checkers. We describe a fully automated translator that takes as input a specification written in template semantics syntax, and a set of template parameters, encoding the specification's semantics, and generates an SMV model of the specification. The result is a parameterized technique for model checking specifications written in a variety of notations. Our work also shows how to represent complex composition operators, such as rendezvous synchronization, in the SMV language, in which there is no matching language construct.

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.

In his habilitation theses Steve Kremer presents some selected research results in the area of formal analysis of security protocols. His contributions include application of formal methods to electronic voting protocols and security APIs, automated methods for verifying equivalence properties, compositional reasoning for security protocols and computational soundness results.

Template semantics is a template-based approach to describing the semantics of model-based notations, where a pre-defined template captures the notations' common semantics, and parameters specify the notations' distinct semantics. In this thesis, we investigate using template semantics to parameterize the translation from a model-based notation to the input language of the SMV family of model checkers. We describe a fully automated translator that takes as input a specification written in template semantics syntax, and a set of template parameters, encoding the specification's semantics, and generates an SMV model of the specification. The result is a parameterized technique for model checking specifications written in a variety of notations. Our work also shows how to represent complex composition operators, such as rendezvous synchronization, in the SMV language, in which there is no matching language construct.

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