ABSTRACT. Security is a top priority at Amazon Web Services. As we have a shared responsibility model with customers, AWS manages the components from the operating system down to the physical security of the facilities; AWS customers are responsible for building secure applications on top of it. In this talk I will describe tools that support our customers in securing their applications, and tools that we use to secure the infrastructure. Under the hood, these tools use formal methods to provide guarantees to our customers.
 

ABSTRACT. We present a novel notion of deadlock for tasks which synchronize on arbitrary boolean conditions and a sound deadlock analysis for it. Contrary to other approaches, our analysis aims to detect dead- locks caused by faulty system design, rather than implementation bugs. A deadlock is a circular dependency between multiple tasks, where a task dependents on a second task, if the execution of this second task enables the first one to resume. This requires the analysis of the side- effects of the computations. The analysis is implemented as an extension to the DECO tool, evaluated for the full coreABS language and uses the KeY-ABS theorem prover to reason about side-effects of computations.

ABSTRACT. Efficient techniques for reachability analysis of timed automata are zone-based methods that explore the reachable state space from the initial state, and SMT-based methods that perform backward search from the target states. It is also possible to perform backward exploration based on zones, but calculating predecessor states for systems with data variables is computationally expensive, prohibiting the successful application of this approach so far. In this paper we overcome this problem by combining the zone-based backward exploration algorithm with the weakest precondition operation for data variables. This combination allows us to handle diagonal constraints efficiently as opposed to zone-based forward search where most approaches require additional operations to ensure correctness. We demonstrate the applicability and compare the efficiency of the algorithm to existing forward exploration approaches by measurements performed on industrial case studies. We show that data variables can be handled efficiently by the weakest precondition operation but the large number of target states often prevents successful verification.

ABSTRACT. In this paper, we present Inductor, a checker for entailments between mutually recursive predicates, whose inductive definitions contain ground constraints belonging to the quantifier-free fragment of Separation Logic. Our tool implements a proof-search method for a cyclic proof system that we have shown to be sound and complete, under certain semantic restrictions involving the set of constraints in a given inductive system. Dedicated decision procedures from the DPLL(T)-based SMT solver CVC4 are used to establish the satisfiability of Separation Logic formulae. Given inductive predicate definitions, an entailment query, and a proof-search strategy, Inductor uses a compact tree structure to explore all derivations enabled by the strategy. A successful result is accompanied by a proof, while an unsuccessful one is supported by a counterexample.

ABSTRACT. Efficient implementations of abstract data types (ADTs) like collections (e.g., key-value stores, sets queues) and synchronization (e.g., signals, semaphores, locks) are essential to modern computing. Programming such objects is however error prone: in minimizing the synchronization overhead among concurrent invocations, one risks violating consistency with their ADTs. Developing automatic validation capable of mitigating such risks is also challenging. Compared to typical safety properties like assertion validity, which are easily verified in linear time per program execution, the runtime verification of consistency generally requires exponential time. Static consistency verification is generally undecidable without bounding the number of concurrent operations, whereas deciding assertion validity only requires bounding implementation state.

In recent works, we have developed scalable and effective methodologies for the specification and verification of concurrent objects. Exploiting the algebraic structure of common ADTs, we demonstrate improved theoretical limits for verification, effective approximations, and practical algorithms for inferring specifications and verifying implementations. Besides enabling tractable verification for many concurrent objects, our work has uncovered novel symbolic characterizations of consistency (e.g., linearizability) checking, which was previously thought to require explicit exponential enumeration (e.g., of possible linearizations).

ABSTRACT. In the development of safety-critical embedded systems, requirements-driven approaches are widely used. Expressing functional requirements in formal languages enables reasoning and formal testing. This paper proposes the Simplified Universal Pattern (SUP) as an easy to use formalism and compares it to SPS, another commonly used specification pattern system. Consistency is an important property of requirements that can be checked already in early design phases. However, formal definitions of consistency are rare in literature and tent to be either too weak or computationally too complex to be applicable to industrial systems. Therefor this work proposes a new formal consistency notion, called partial consistency, for the SUP that is a trade-off between exhaustiveness and complexity. Partial consistency identifies critical cases and verifies if these cause conflicts between requirements.

ABSTRACT. The Internet of Things (IoT) promises a revolution in the monitoring and control of a wide range of applications, from urban water supply networks and precision agriculture food production, to vehicle connectivity and healthcare monitoring. For applications in such critical areas, control software and protocols for IoT systems must be verified to be both robust and reliable. Two of the largest obstacles to robustness and reliability in IoT systems are effects on the hardware caused by environmental conditions, and the choice of parameters used by the protocol. In this paper we use probabilistic model checking to verify that a synchronisation and dissemination protocol for Wireless Sensor Networks (WSNs) is correct with respect to its requirements, and is not adversely affected by the environment. We show how the protocol can be converted into a logical model and then analysed using the probabilistic model-checker, PRISM. Using this approach we prove under which circumstances the protocol is guaranteed to synchronise all nodes and disseminate new information to all nodes. We also examine the bounds on synchronisation as the environment changes the performance of the hardware clock, and investigate the scalability constraints of this approach.

ABSTRACT. During a course on model checking we developed BMoth, a full-stack model checker for classical B, featuring both explicit-state and symbolic model checking. Given that we only had a single university term to finish the project, a particular focus was on reusing existing libraries to reduce implementation workload.

In the following, we report on a selection of reusable libraries, which can be combined into a prototypical model checker relatively easily. Additionally, we discuss where custom code depending on the specification language to be checked is needed and where further optimization can take place. To conclude, we compare to other model checkers for classical B.