This project created a program that takes predicate calculus formulas and creates a visual Semantic Tableaux truth tree, thereby proving or disproving a conclusion. Formal methods used in developing and verifying software and hardware are mathematically based techniques for describing and reasoning about system properties. Such formal methods provide frameworks within which people specify, develop, and verify systems in a systematic, rather than ad hoc, manner. Formal methods include the more specific activities of program specification, program verification and hardware verification.

<p>The complex behavior of computer systems offers many challenges for <i>formal verification</i>. The analysis quickly becomes difficult as the number of participating processes increases.</p><p>A <i>parameterized system</i> is a family of systems parameterized on a number <i>n</i>, typically representing the number of participating processes. The <i>uniform verification problem</i> — to check whether a property holds for each instance — is an infinite-state problem. The automated analysis of parameterized and infinite-state systems has been the subject of research over the last 15–20 years. Much of the work has focused on safety properties. Progress in verification of liveness properties has been slow, as it is more difficult in general.</p><p>In this thesis, we consider verification of parameterized and infinite-state systems, with an emphasis on liveness, in the verification framework called <i>regular model checking (RMC)</i>. In RMC, states are represented as words, sets of states as regular expressions, and the transition relation as a regular relation.</p><p>We extend the automata-theoretic approach to RMC. We define a <i>specification logic</i> sufficiently strong to specify systems representable using RMC, and linear temporal logic properties of such systems, and provide an automatic translation from a specification into an analyzable model.</p><p>We develop <i>acceleration techniques</i> for RMC which allow more uniform and automatic verification than before, with greater power. Using these techniques, we succeed to verify safety and liveness properties of parameterized protocols from the literature.</p><p>We present a novel <i>reachability based</i> verification method for verification of liveness, in a general setting. We implement the method for RMC, with promising results.</p><p>Finally, we develop a framework for the verification of dynamic networks based on graph transformation, which generalizes the systems representable in RMC. In this framework we verify the latest version of the DYMO routing protocol, currently being considered for standardization by the IETF.</p>

Reuse of software designs, experience and components is essential to making substantial improvements in software productivity, development cost, and quality. However, the many facets of reuse are still rarely used in the various phases of the software development lifecycle because of a lack of adequate theories, processes, and tools to support consistent application of reuse concepts. There is a need for approaches including definitions, models and properties of reuse that would provide explicit guidance to a software development team in applying reuse. In particular there is a need to provide abstractions that clearly separate the various functional concerns addressed in a software system. Separating concerns simplifies the identification of the software components that can benefit from reuse and can provide guidance on how reuse may be applied. In this thesis we present an extended model related to the separation of concerns in object-oriented design. The model, called views, indicates how an object-oriented design can be clearly separated into objects and their corresponding interfaces. In this model objects can be designed so that they are independent of their environment, because adaptation to the environment is the responsibility of the interface or view. The view can be seen as expressing the semantics for the 'glue' that joins components or objects together to create a software system. Informal versions of the views model have already been successfully applied to operational and commercial software systems. The objective of this thesis is to provide the views notion with a theoretical foundation to address reuse and separation of concerns. After clearly defining the views model we show the formal approach to combining the objects, interfaces (views), and their interconnection into a complete software system. The objects and interfaces are defined using an object calculus based on temporal logic, while the interconnections among object and views are specified using category theory. This formal framework provides the mathematical foundation to support the verification of the properties of both the components and the composite software system. We then show how verification can be mechanized by converting the formal version of the views model into higher-order logic and using PVS to support mechanical proofs.

The precision of formal specifications allows us to prove program correctness. Even if formal methods are not used throughout the software project, formalisation improves our understanding of the problem. Formal specifications are amenable to automated analysis and consistency checking. However using them is challenging. Customers do not understand formal notations. Specifiers have difficulty tackling large problems. Once systems are built, formal specifications quickly become outdated during software maintenance. A method of developing formal specifications using concrete scenarios is proposed to tackle the disadvantages just mentioned. A concrete scenario describes system behaviour with successive steps. The pre- and post-states of scenario steps are expressed with actual data rather than variables. Concrete scenarios are expressed in a natural language or formal notation. They increase customer involvement in the creation of formal specifications. Scenarios may be ranked by priorities allowing specifiers to focus on a small part of the system. Formal specifications are constructed incrementally. New requirements are also captured in concrete scenarios which guide the modification of formal specifications. On one hand, concrete scenarios assist the creation and maintenance of formal specifications. On the other hand, they facilitate program correctness proofs without using conventional formal specifications. This is achieved by adding implementation details to customer scenarios. The resulting developer scenarios, encapsulating decisions of data structures and algorithms, are generalised to operation schemas. With the implementation details, the schemas written in formal notations are programs rather than specifications.

Business Process Modelling Notation (BPMN) is a standardised diagram notation for modelling interactive workflow processes graphically at the design stage. The primary objective of this thesis is to provide a framework for precise specifications and formal verifications of workflow processes modelled as BPMN diagrams. We provide two behavioural semantics for BPMN in the process algebra Communicating Sequential Processes (CSP). We apply existing CSP refinement orderings to both the refinement of business process diagrams and the verification of behavioural compatibility of business process collaborations. The first semantic model is an untimed model, focusing on the control flow and communication of business processes. The second semantic model extends the first one to capture the timing aspect of behaviour. We also consider the applications of the semantic models. The secondary objective of this thesis is to apply BPMN and the semantic models to reason about long running empirical studies (e.g. laboratory experiments, clinical trials). We introduce a declarative workflow model Empiricol for recording trials and experiments precisely, and define bidirectional transformation functions between BPMN and Empiricol. Using the transformation functions, we make graphical specification, simulation, automation and verification of trials and experiments possible. We provide two case studies on the applications of BPMN’s formalisations.

Engineering contemporary distributed software applications is a challenging task due to the dynamic operating conditions in which these systems have to function. Examples are dynamic availability of resources, errors that are difficult to predict, and changing user requirements. These dynamics can affect a number of quality concerns of a system, such as robustness, openness, and performance. The challenges of engineering software systems with such dynamics have motivated the need for self-adaptation. Self-adaptation is based on the principle of separation of concerns, distinguishing two well defined systems: a managed system that deals with domain specific concerns and a managing system that deals with particular quality concerns of the managed system through adaptation with a feedback loop. State of the art in self- adaptation advocates the use of formal methods to specify and verify the system's behavior in order to provide evidence that the system's goals are satisfied. However, little work has been done on the consolidation of design knowledge to model and verify self-adaptation behaviors. To support designers, this thesis contributes with a set of formally specified templates for the specification and verification of self-adaptive behaviors of a family of distributed self-adaptive systems. The templates are based on the MAPE-K reference model (Monitor-Analyze-Plan-Execute plus Knowledge). The templates comprise: (1) behavior specification patterns for modeling the different MAPE components of a feedback loop, and (2) property specification patterns that support verification of the correctness of the adaptation behaviors. The target domain are distributed applications in which self-adaptation is used for managing resources for robustness and openness requirements. The templates are derived from expertise with developing several self-adaptive systems, including a collaborative mobile learning application in which we have applied self-adaptation to make the system robust to degrading GPS accuracy, and a robotic system in which we apply self-adaptation to support different types of openness requirements. We demonstrate the reusability of the templates in a number of case studies. / AMULETS

Increasing amounts of data are being collected and stored relating to every aspect of an individual's life, ranging from shopping habits to medical conditions. This data is increasingly being shared for a variety of reasons, from providing vast quantities of data to validate the latest medical hypothesis, to supporting companies in targeting advertising and promotions to individuals that fit a certain profile. In such cases, the data being used often comes from multiple sources --- with each of the contributing parties owning, and being legally responsible for, their own data. Within such models of collaboration, access control becomes important to each of the individual data owners. Although they wish to share data and benefit from information that others have provided, they do not wish to give away the entirety of their own data. Rather, they wish to use access control policies that give them control over which aspects of the data can be seen by particular individuals and groups. Each data owner will have access control policies that are carefully crafted and understood --- defined in terms of the access control representation that they use, which may be very different from the model of access control utilised by other data owners or by the technology facilitating the data sharing. Achieving interoperability in such circumstances would typically require the rewriting of the policies into a uniform or standard representation --- which may give rise to the need to embrace a new access control representation and/or the utilisation of a manual, error-prone, translation. In this thesis we propose an alternative approach, which embraces heterogeneity, and establishes a framework for automatic transformations of access control policies. This has the benefit of allowing data owners to continue to use their access control paradigm of choice. Of course, it is important that the data owners have some confidence in the fact that the new, transformed, access control policy representation accurately reflects their intentions. To this end, the use of tools for formal modelling and analysis allows us to reason about the translation, and demonstrate that the policies expressed in both representations are equivalent under access control requests; that is, for any given request both access control mechanisms will give an equivalent access decision. For the general case, we might propose a standard intermediate access control representation with transformations to and from each access control policy language of interest. However, for the purpose of this thesis, we have chosen to model the translation between role-based access control (RBAC) and the XML-based policy language, XACML, as a proof of concept of our approach. In addition to the formal models of the access control mechanisms and the translation, we provide, by way of a case study, an example of an implementation which performs the translation. The contributions of this thesis are as follows. First, we propose an approach to resolving issues of authorisation heterogeneity within distributed contexts, with the requirements being derived from nearly eight years of work in developing secure, distributed systems. Our second contribution is the formal description of two popular approaches to access control: RBAC and XACML. Our third contribution is the development of an Alloy model of our transformation process. Finally, we have developed an application that validates our approach, and supports the transformation process by allowing policy writers to state, with confidence, that two different representations of the same policy are equivalent.

Many software systems exhibit probabilistic behaviour, either added explicitly, to improve performance or to break symmetry, or implicitly, through interaction with unreliable networks or faulty hardware. When employed in safety-critical applications, it is important to rigorously analyse the behaviour of these systems. This can be done with a formal verification technique called model checking, which establishes properties of systems by algorithmically considering all execution scenarios. In the presence of probabilistic behaviour, we consider quantitative properties such as "the worst-case probability that the airbag fails to deploy within 10ms", instead of qualitative properties such as "the airbag eventually deploys". Although many model checking techniques exist to verify qualitative properties of software, quantitative model checking techniques typically focus on manually derived models of systems and cannot directly verify software. In this thesis, we present two quantitative model checking techniques for probabilistic software. The first is a quantitative adaptation of a successful model checking technique called counter-example guided abstraction refinement which uses stochastic two-player games as abstractions of probabilistic software. We show how to achieve abstraction and refinement in a probabilistic setting and investigate theoretical extensions of stochastic two-player game abstractions. Our second technique instruments probabilistic software in such a way that existing, non-probabilistic software verification methods can be used to compute bounds on quantitative properties of the original, uninstrumented software. Our techniques are the first to target real, compilable software in a probabilistic setting. We present an experimental evaluation of both approaches on a large range of case studies and evaluate several extensions and heuristics. We demonstrate that, with our methods, we can successfully compute quantitative properties of real network clients comprising approximately 1,000 lines of complex ANSI-C code — the verification of such software is far beyond the capabilities of existing quantitative model checking techniques.

Le contrôle d'accès permet de spécifier une partie de la politique de sécurité d'un SI (système d'informations). Une politique de CA (Contrôle d'accès) permet de définir qui a accès à quoi et sous quelles conditions. Les concepts fondamentaux utilisés en CA sont : les permissions, les interdictions (ou prohibitions), les obligations et la SoD (séparation des devoirs). Les permissions permettent d'autoriser une personne à accéder à des ressources. Au contraire les prohibitions interdisent à une personne d'accéder à certaines ressources. Les obligations lient plusieurs actions. Elles permettent d'exprimer le fait qu'une action doit être réalisée en réponse à une première action. La SoD permet de sécuriser une procédure en confiant la réalisation des actions composant cette procédure à des agents différents. Différentes méthodes de modélisation de politiques de contrôle d'accès existent. L'originalité de la méthode EB3Sec issue de nos travaux repose sur deux points :- permettre d'exprimer tous les types de contraintes utilisées en CA dans un même modèle,- proposer une approche de modélisation basée sur les événements. En effet, aucune des méthodes actuelles ne présente ces deux caractéristiques, au contraire de la méthode EB3Sec. Nous avons défini un ensemble de patrons, chacun des patrons correspond à un type de contraintes de CA. Un modèle réalisé à l'aide de la méthode EB3Sec peut avoir différentes utilisations :- vérification et simulation,- implémentation. La vérification consiste à s'assurer que le modèle satisfait bien certaines propriétés, dont nous avons défini différents types. Principalement, les blocages doivent être détectés. Ils correspondent à des situations où une action n'est plus exécutable ou à des situations où plus aucune action n'est exécutable. Les méthodes actuelles des techniques de preuves par vérification de modèles ne permettent pas de vérifier les règles dynamiques de CA. Elles sont alors combinées à des méthodes de simulation. Une fois qu'un modèle a été vérifié, il peut être utilisé pour implémenter un filtre ou noyau de sécurité. Deux manières différentes ont été proposées pour réaliser cette implémentation : transformer le modèle EB3Sec vers un autre langage, tel XACML, possédant une implémentation ayant déjà atteint la maturité ou réaliser un noyau de sécurité utilisant le langage EB3Sec comme langage d'entrée / Access control allows one to specify a part of the security Policy of an IS (information system). An AC (access control) policy defines which conditions must old for someone to have access to something. Main concepts used in AC are: permissions, prohibitions, obligations and SoD (separation of duty). Permissions allow someone to access to some resources. On the opposite, prohibitions forbid users to have access to some resources. Obligations link at least two actions: when a user performs an action, he must perform another one. SoD secures an action by dividing it in different tasks, and entrusting the execution of these tasks to different users. Many AC policies modelling methods already exist. The main particularities of the EB3Sec methods are:- All AC concepts can be expressed in a unique model,- This modelling method is event-based. No existing AC modelling methods presents these two characteristics. We define a set of patterns; each pattern corresponds to a specific AC constraint. An EB3Sec model can be used for different purposes:- Simulation and verification,- Implementation.Verifying a model consists in checking that the model complies with some properties that we have defined. Mainly, blocking must be detected. Blocking corresponds to a step of execution where no action can be executed or to situations where an action cannot be performed anymore. Current model checking methods cannot be used to check properties on dynamic AC constraints. Thus, model-checking techniques are combined to simulation techniques. Once a model is verified, it can be transformed in an implementation. To implement an EB3Sec model two ways can be considered: the EB3Sec model can be translated into an other language, such as XACML, which possesses a mature implementation, or a security kernel using EB3Sec as input language can be implemented

Approved for public release, distribution is unlimited / Cryptographic protocols provide security services through the application of cryptography. When designing a cryptographic protocol, the requirements are, often, specified informally. Informal specification can lead to incorrect protocols from misinterpreting the security requirements and environmental assumptions. Formal tools have been shown to reduce ambiguity. In this paper, a cryptographic protocol, called the Secure Open Distribution Protocol (SODP), is developed to provide authentication services for open source information. A formal development process is proposed to aid in the design of the SODP. The Strand Space method has been selected as the formal mechanism for specifying requirements, architecting a protocol design, and assuring the correctness of the protocol. First, the informal authentication requirements are modeled as agreement properties. Next, Authentication Tests, a Strand Space concept, are introduced to aid in the design of the SODP. Finally, a formal proof is constructed to assure that the SODP has satisfied all requirements. The result of the development process proposed in this paper is a cryptographic protocol that can be used to securely distribute open source information. Also, the Strand Space method is demonstrated as a viable option for the formal development of a cryptographic protocol. / Civilian, Federal Cyber Corps