RV-Android is a new freely available open source runtime library for monitoring formal safety properties on Android. RV-Android uses the commercial RV-Monitor technology as its core monitoring library generation technology, allowing for the verification of safety properties during execution and operating entirely in userspace with no kernel or operating system modifications required. RV-Android improves on previous Android monitoring work by replacing the JavaMOP framework with RV-Monitor, a more advanced monitoring library generation tool with core algorithmic improvements that greatly improve resource consumption, efficiency, and battery life considerations. We demonstrate the developer usage of RV-Android with the standard Android build process, using instrumentation mechanisms effective on both Android binaries and source code. Our method allows for both property development and advanced application testing through runtime verification. We showcase the user frontend of RV-Monitor, which is available for public demo use and requires no knowledge of RV concepts. We explore the extra expressiveness the MOP paradigm provides over simply writing properties as aspects through two sample security properties, and show an example of a real security violation mitigated by RV-Android on-device. Lastly, we propose RV as an extension to the next-generation Android permissions system debuting in Android M.

Despite the numerous static and dynamic program analysis techniques in the literature, data races remain one of the most common bugs in modern concurrent software. Further, the techniques that do exist either have limited detection capability or are unsound, meaning that they report false positives. We present a sound race detection technique that achieves a provably higher detection capability than existing sound techniques. A key insight of our technique is the inclusion of abstracted control flow information into the execution model, which increases the space of the causal model permitted by classical happens-before or causally-precedes based detectors. By encoding the control flow and a minimal set of feasibility constraints as a group of first-order logic formulae, we formulate race detection as a constraint solving problem. Moreover, we formally prove that our formulation achieves the maximal possible detection capability for any sound dynamic race detector with respect to the same input trace under the sequential consistency memory model. We demonstrate via extensive experimentation that our technique detects more races than the other state-of-the-art sound race detection techniques, and that it is scalable to executions of real world concurrent applications with tens of millions of critical events. These experiments also revealed several previously unknown races in real systems (e.g., Eclipse) that have been confirmed or fixed by the developers. Our tool is also adopted by Eclipse developers.

Runtime verification can effectively increase the reliability of software systems. In recent years, parametric runtime verification has gained a lot of traction, with several systems proposed. However, lack of real specifications and prohibitive runtime overhead when checking numerous properties simultaneously prevent developers or users from using runtime verification. This paper reports on more than 150 formal specifications manually derived from the Java API documentation of commonly used packages, as well as a series of novel techniques which resulted in a new runtime verification system, RV-Monitor. Experiments show that these specifications are useful for finding bugs and bad software practice, and RV-Monitor is capable of monitoring all our specifications simultaneously, and runs substantially faster than other state-of-the-art runtime verification systems.

Early efforts in runtime verification show that parametric regular and temporal logic specifications can be monitored efficiently. These approaches, however, have limited expressiveness: their specifications always reduce to monitors with finite state. More recent developments showed that parametric context-free properties can be efficiently monitored with overheads generally lower than 12-15%. While context-free grammars are more expressive than finite-state languages, they still do not allow every computable safety property. This paper presents a monitor synthesis algorithm for string rewriting systems (SRS). SRSs are well known to be Turing complete, allowing for the formal specification of any computable safety property. Earlier attempts at Turing complete monitoring have been relatively inefficient. This paper demonstrates that monitoring parametric SRSs is practical. The presented algorithm uses a modified version of Aho-Corasick string searching for quick pattern matching with an incremental rewriting approach that avoids reexamining parts of the string known to contain no redexes.

Runtime monitoring is an effective means to improve the reliability of systems. In recent years, parametric monitoring, which is highly suitable for object-oriented systems, has gained significant traction. Previous work on the performance of parametric runtime monitoring has focused on the performance of monitoring only one specification at a time. A realistic system, however, has numerous properties that need to be monitored simultaneously. This paper introduces scalable techniques to improve the performance of one of the fastest parametric monitoring systems, JavaMOP, in the presence of multiple simultaneous properties, resulting in average runtime overheads that are less than the summation of the overheads of the properties run in isolation. An extensive evaluation shows that these techniques, which were derived following a thorough investigation and analysis of the current bottlenecks in JavaMOP, improve its runtime performance in the presence of multiple properties by up to two times and the memory usage by 34%.

Runtime monitoring is a technique usable in all phases of the software development cycle, from initial testing, to debugging, to actually maintaining proper function in production code. Of particular importance are parametric monitoring systems, which allow the specification of properties that relate objects in a program, rather than only global properties. In the past decade, a number of parametric runtime monitoring systems have been developed. Here we give a demonstration of our system, JavaMOP. It is the only parametric monitoring system that allows multiple differing logical formalisms. It is also the most efficient in terms of runtime overhead, and very competitive with respect to memory usage.

Software security attacks represent an ever growing problem. One way to make software more secure is to use Inlined Reference Monitors (IRMs), which allow security specifications to be inlined inside a target program to ensure its compliance with the desired security specifications. The IRM approach has been developed primarily by the security community. Runtime Verification (RV), on the other hand, is a software engineering approach, which is intended to formally encode system specifications within a target program such that those specifications can be later enforced during the execution of the program. Until now, the IRM and RV approaches have lived separate lives; in particular RV techniques have not been applied to the security domain, being used instead to aid program correctness and testing. This paper discusses the usage of a formalism-generic RV system, JavaMOP, as a means to specify IRMs, leveraging the careful engineering of the JavaMOP system for ensuring secure operation of software in an efficient manner.

Formal specication of correct library usage is extremely useful, both for software developers and for the formal analysis tools they use, such as model checkers or runtime monitoring systems. Unfortunately, the process of creating formal specications is time consuming, and, for the most part, even the libraries in greatest use, such as the Java Development Kit (JDK) standard library, are left wholly without formal specication. This paper presents a tool-supported approach to help writing formal specications for Java libraries and creating documentation augmented with highlighting and formal specications. The presented approach has been applied to systematically and completely formalize the runtime properties of three core and commonly used packages of the JDK API, namely java.io, java.lang and java.util, yielding 137 formal specications. Indirectly, this paper also brings empirical evidence that parametric specications may be suciently powerful to express virtually all desirable runtime properties of the JDK API, and that its informal documentation can be formalized.

This article gives an overview of the, monitoring oriented programming framework (MOP). In MOP, runtime monitoring is supported and encouraged as a fundamental principle for building reliable systems. Monitors are automatically synthesized from specified properties and are used in conjunction with the original system to check its dynamic behaviors. When a specification is violated or validated at runtime, user-defined actions will be triggered, which can be any code, such as information logging or runtime recovery. Two instances of MOP are presented: JavaMOP (for Java programs) and BusMOP (for monitoring PCI bus traffic). The architecture of MOP is discussed, and an explanation of parametric trace monitoring and its implementation is given. A comprehensive evaluation of JavaMOP attests to its efficiency, especially in comparison with similar systems. The implementation of BusMOP is discussed in detail. In general, BusMOP imposes no runtime overhead on the system it is monitoring.

Parametric properties are behavioral properties over program events that depend on one or more parameters. Parameters are bound to concrete data or objects at runtime, which makes parametric properties particularly suitable for stating multi-object relationships or protocols. Monitoring parametric properties independently of the employed formalism involves slicing traces with respect to parameter instances and sending these slices to appropriate non-parametric monitor instances. The number of such instances is theoretically unbounded and tends to be enormous in practice, to an extent that how to efficiently manage monitor instances has become one of the most challenging problems in runtime verification. The previous formalism-independent approach was only able to do the obvious, namely to garbage collect monitor instances when all bound parameter objects were garbage collected. This led to pathological behaviors where unnecessary monitor instances were kept for the entire length of a program. This paper proposes a new approach to garbage collecting monitor instances. Unnecessary monitor instances are collected lazily to avoid creating undue overhead. This lazy collection, along with some careful engineering, has resulted in RV, the most efficient parametric monitoring system to date. Our evaluation shows that the average overhead of RV in the DaCapo benchmark is 15%, which is two times lower than that of JavaMOP and orders of magnitude lower than that of Tracematches.

This paper describes a formal executable semantics for the Verilog hardware description language. The goal of our formalization is to provide a concise and mathematically rigorous reference augmenting the prose of the official language standard, and ultimately to aid developers of Verilog-based tools; e.g., simulators, test generators, and verification tools. Our semantics applies equally well to both synthesizeable and behavioral designs and is given in a familiar, operational-style within a logic providing important additional benefits above and beyond static formalization. In particular, it is executable and searchable so that one can ask questions about how a, possibly nondeterministic, Verilog program can legally behave under the formalization. The formalization should not be seen as the final word on Verilog, but rather as a starting point and basis for community discussions on the Verilog semantics.

Recent developments in runtime verification and monitoring show that parametric regular and temporal logic specifications can be efficiently monitored against large programs. However, these logics reduce to ordinary finite automata, limiting their expressivity. For example, neither can specify structured properties that refer to the call stack of the program. While context-free grammars (CFGs) are expressive and well-understood, existing techniques for monitoring CFGs generate large runtime overhead in real-life applications. This paper demonstrates that monitoring parametric CFGs is practical (with overhead on the order of 12% or lower in most cases). We present a monitor synthesis algorithm for CFGs based on an LR(1) parsing algorithm, modified to account for good prefix matching. In addition, a logic-independent mechanism is introduced to support matching against the suffixes of execution traces.

The RV system is the first system to merge the benefits of Runtime Monitoring with Predictive Analysis. The Runtime Monitoring portion of RV is based on the successful Monitoring Oriented Programming system developed at the University of Illinois [6,7,9,21,5], while the Predictive Analysis capability is a vastly expanded version of the jPredictor System also developed at the University of Illinois [11,14].With the RV system, runtime monitoring is supported and encouraged as a fundamental principle for building reliable software: monitors are automatically synthesized from specified properties and integrated into the original system to check its dynamic behaviors. When certain conditions of interest occur, such as a violation of a specification, user-defined actions will be triggered, which can be any code from information logging to runtime recovery. The RV system supports the monitoring of parametric properties that may specify a relationship between objects. Properties may be defined using one of several logical formalisms, such as: extended regular languages, context-free patterns, deterministic finite state machines, linear temporal logic, and past time linear temporal logic. The system is designed in such a way that adding new logical formalisms is a relatively simple taskThe predictive capabilities allow any of these monitoring specifications to be extended to checking not just the actual runtime traces of program execution, but any trace that may be inferred from a constructed casual model. The Predictive Analysis also features built in algorithms for race detection and atomicity violations, that are both highly useful in concurrent system design and difficult to specify in terms of formal specification languages.

Parametric properties provide an effective and natural means to describe object-oriented system behaviors, where the parameters are typed by classes and bound to object instances at runtime. Efficient monitoring of parametric properties, in spite of increasingly growing interest due to applications such as testing and security, imposes a highly non-trivial challenge on monitoring approaches due to the potentially huge number of parameter instances. Existing solutions usually compromise their expressiveness for performance or vice versa. In this paper, we propose a generic, in terms of specification formalism, yet efficient, solution to monitoring parametric specifications. Our approach is based on a general algorithm for slicing parametric traces and makes use of static knowledge about the desired property to optimize monitoring. The needed knowledge is not specific to the underlying formalism and can be easily computed when generating monitoring code from the property. Our approach works with any specification formalism, providing better and extensible expressiveness. Also, a thorough evaluation shows that our technique outperforms other state-of-art techniques optimized for particular logics or properties.

This paper gives a brief overview of Monitoring Oriented Programming (MOP). In MOP, runtime monitoring is supported and encouraged as a fundamental principle for building reliable software: monitors are automatically synthesized from specied properties and integrated into the original system to check its dynamic behaviors. When a specication is violated or validated at runtime, user-dened actions will be triggered, which can be any code from information logging to runtime recovery. Two instances of MOP are introduced: JavaMOP (for Java programs) and BusMOP (for monitoring PCI bus trac). The architecture of MOP is discussed, and a brief explanation of parametric trace monitoring and its implementation is given. Finally, a comprehensive evaluation of JavaMOP attests to its eciency, especially with respect to similar systems; BusMOP, in general, imposes 0 runtime overhead on the system it is monitoring.

System-on-Chip (SoC) is a promising paradigm to implement safety-critical embedded systems, but it poses significant challenges from a design and verification point of view. In particular, in a mixed-criticality system, low criticality applications must be prevented from interfering with high criticality ones. In this paper, we introduce a new design methodology for SoC that provides strong isolation guarantees to applications with different criticalities. A set of certificates describing the assumed application behavior is extracted from a functional Architectural Analysis and Design Language (AADL) specification. Our tools then automatically generate hardware wrappers that enforce at run-time the behavior described by the certificates. In particular, we employ run-time monitoring to formally check all data communication in the system, and we enforce timing reservations for both computation and communication resources. Verification is greatly simplified because certificates are much simpler than the components used to implement low-criticality applications. The effectiveness of our methodology is proven on a case study consisting of a medical pacemaker.