ABSTRACT. The Windows Driver Verification Platform (DVP) provides compile time and runtime technologies for verifying that device drivers work correctly: Static Driver Verifier (SDV) is a compile time verification tool available for 3rd party developers as part of the Windows Driver Development kit.  Runtime Driver Verifier (DV) is integrated directly into the Windows OS and shipped inbox. Both technologies are used by 3rd party driver developers as well as internally at Microsoft and in the entire range of Window devices from IoT devices and all the way up to Microsoft Azure deployments.

Whereas verification paradigms, engines, and abilities are different between SDV and DV, these technologies share a common concept of interface rules between the OS kernel and drivers (kernel extensions, in general). The interface is materialized by a set of APIs supplied by the kernel and sets of callbacks supplied by drivers.  In a narrow sense, each of the two technologies is aimed at verifying that drivers follow the interface rules.

The talk will cover the current state of the platform, shared features of the two technologies and their differences.   We will also discuss our pipeline for technology transfer from Microsoft Research to Windows.

ABSTRACT. CSP_E is a specification language for runtime monitors that can directly express concurrency in a bottom-up manner that composes the system from simpler, interacting components. It includes constructs to explicitly flag failures to the monitor, which unlike deadlocks and live-locks in conventional process algebras, propagate globally and aborts the whole system’s execution. Although CSP_E has a trace semantics along with an implementation demonstrating acceptable performance, it lacks an operational semantics. An operational semantics is not only more accessible than trace semantics but also indispensable for ensuring the correctness of the implementation. Furthermore, a process algebra like CSP_E admits multiple denotational semantics appropriate for different purposes, and an operational semantics is the basis for justifying such semantics’ integrity and relevance. In this paper, we develop an SOS-style operational semantics for CSP_E , which properly accounts for explicit failures and will serve as a basis for further study of its properties, its optimization, and its use in runtime verification.

ABSTRACT. We present HySIA: a reliable runtime verification tool for nonlinear hybrid automata (HA) and signal temporal logic (STL) properties. HySIA simulates an HA with interval analysis techniques so that a trajectory is enclosed sharply within a set of intervals. Then, HySIA computes whether the simulated trajectory satisfies a given STL property; the computation is performed again with interval analysis to achieve reliability. Simulation and verification using HySIA are demonstrated through several example HA and STL formulas.

ABSTRACT. In this paper, we discuss the feasibility of monitoring partially synchronous distributed systems to detect latent bugs, i.e., errors caused by concurrency and race conditions among concurrent processes. We present a monitoring framework where we model both system constraints and latent bugs as Satisfiability Modulo Theories (SMT) formulas, and we detect the presence of latent bugs using an SMT solver. We demonstrate the feasibility of our framework using both synthetic applications where latent bugs occur at any time with random probability and an application involving exclusive access to a shared resource with a subtle timing bug. We illustrate how the time required for verification is affected by parameters such as communication frequency, latency, and clock skew. Our results show that our framework can be used for real-life applications, and because our framework uses SMT solvers, the range of appropriate applications will increase as these solvers become more efficient over time.

ABSTRACT. State-of-the-art memory debuggers have become efficient in detecting spatial memory errors - dereference of pointers to unallocated memory. These tools, however, cannot always detect errors arising from the use of stale pointers to valid memory (temporal memory errors). This paper presents an approach to sound detection of temporal memory errors during a run of a program. This technique operates by tracking memory allocated by a program tagging allocated objects and program pointers with tokens that allow to reason about their temporal properties. The technique further checks pointer dereferences and detects temporal (and spatial) memory errors before they occur. The present approach has been implemented in E-ACSL - a runtime verification tool for C programs. Experimentation with E-ACSL using TempLIST benchmark comprising small C programs seeded with temporal errors shows that the suggested technique can detect temporal memory errors missed by state-of-the-art memory debuggers. Further experiments with computationally intensive runs of programs from SPEC CPU indicate that the overheads of the proposed approach are within acceptable range to be used during testing or debugging.

ABSTRACT. A certifying algorithm produces for an input x an output y and additionally a witness w. If a witness predicate holds for the triple (x, y, w), then the output y is correct. A checker algorithm decides the witness predicate at runtime. Thus, a certifying algorithm is a runtime verification technique. While certifying sequential algorithms are well-established, we consider distributed algorithms which behave differently. For instance, their output is distributed over a network. To verify such an output, we transfer the concept of certification to distributed algorithms. In this paper, we define certifying distributed algorithms that certify their output. To this end, a witness predicate states a property in the network from which the correctness follows. For distributed checking of the witness predicate, we give predicates which can be decided for each component. Since the witness is computed and checked in a distributed manner, we exploit distribution. We illustrate the applicability by examples.

ABSTRACT. Software-defined networking (SDN) is transforming the way networks are managed, as fixed distributed protocols give way to flexible, centralized route calculation software. This shift brings to the forefront the issue of software implementation errors, which may produce wrong routes that cause significant network disruption. We propose a formal run-time certification mechanism that rejects any wrongly calculated route before it is installed in the network. Certification is done through a strategy called witnessing, where a witness (i.e., a justification) is provided by the route calculation software for every routing decision. Witnesses are validated against the desired user intent using a formal network model before any changes are installed on the real network. This strategy shifts trust away from the complex system software to a simple checker, whose functionality can be formally validated. We define a language to specify connection-based user requests (``intents''), witnesses for each type of intent, and the checking algorithm. We also formulate a notion of refinement between networks, and show that it preserves the realizability of intents across abstraction levels. That allows route calculation algorithms to operate effectively on small abstract networks which hide network complexity, with the guarantee that the calculated abstract routes are also realizable in the real network.

ABSTRACT. Small unmanned vehicles support use cases ranging from disaster recovery, to infrastructure mapping, to surveillance and recon. The provenance of the hardware and the software on these systems is usually not known, and operators are often not verticle experts in the technologies of such systems. Furthermore, the devices can be deployed in environments that are contested. Yet, the benefits of these systems outweigh the perceived risks stemming from these concerns, so much so that critical tasks and data are routinely delegated to these systems based mostly on faith, and without a sound technological basis for determining if a device is trustworthy. This paper describes an approach that can determine an operator's trust in a mission system. The Composable and Measurable view of Trust approach applies continuous monitoring to provide an indication of whether a mission system is performing within a trusted operating region. In an implementation and initial evaluation we show that for a given mission, it is possible to (a) define a multi-dimensional trusted operating region, (b) monitor the system during an ongoing mission, and (c) detect when anomalous effects put the mission at risk.

ABSTRACT. Policy enforcers are sophisticated runtime components that can prevent failures by enforcing the correct behavior of the software. While a single enforcer can be easily designed focusing only on the behavior of the application that must be monitored, the effect of multiple enforcers that enforce different policies might be hard to predict. So far, mechanisms to resolve interferences between enforcers have been based on priority mechanisms and similar heuristics. Although these methods provide a mechanism to take decisions when two enforcers try to affect the execution at a same time, they do not guarantee the lack of interference on the global behavior of the system. In this paper, we present a verification strategy that can be exploited to discover interferences between sets of enforcers and thus safely identify a-priori the enforcers that can co-exist. In our evaluation, we experimented our verification method with several policy enforcers for Android and successfully discovered some incompatibilities.

ABSTRACT. SSO (single-sign-on) services, such as those provided by Facebook, Google and Microsoft Azure, are integrated into tens of millions of websites and cloud services, just like the front door lock for every home. Imagine you are a website developer, typically unfamiliar with SSO protocols. Your manager wants you to integrate a particular SSO service onto a website written in a particular language (e.g., PHP, ASP.NET or Python). You are likely overwhelmed by the amount of work for finding a suitable SSO library, understanding its programming guide, and writing your code. Moreover, studies have shown that many SSO integrations on real-world websites are incorrect, and thus vulnerable to security attacks! SVAuth is an open-source project that tries to provide integration solutions for all major SSO services in all major web languages. Its correctness is ensured by a technology called self-verifying execution, which performs program verification at runtime. SVAuth is so easy to adopt that a website developer does not need any knowledge about SSO protocols or implementations. This paper describes the architecture of SVAuth and how to use it on real-world websites.

ABSTRACT. The design of the user interface of a modern application needs to follow a set of guidelines, codified in a document published by the maintainers of a particular operating system. These guidelines are intended to ensure a minimum level of quality and consistency across applications. Unfortunately, ensuring compliance to these guidelines is left to the application developer, and is generally done by manual testing. In this paper, we present a methodology, based on runtime verification, for the automated testing of user interface guidelines of Android applications.

ABSTRACT. Wingman is a run-time monitoring system that aims to detect and mitigate anomalies, including malware infections, within virtual appliances (VAs). It uses virtual-machine introspection (VMI) to observe the kernel state of a monitored VA, and it uses an expert system to determine when that state represents an anomaly. Wingman does not simply restart a compromised VA; instead, it attempts to repair the VA, thereby minimizing potential VA downtime and state loss. This paper presents the Wingman system that combines kernel-level observations, application-specific knowledge, and components outside and inside a monitored VA. It presents experiments in which Wingman detected and mitigated four different types of malware within a web-server appliance. For each attack, Wingman was able to bring the VA into an acceptable state, defending the VA until a system administrator can deploy a permanent repair.