Publications

Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment of nfer. The evaluation problem asks whether a given interval is generated by applying rules to a known input, while the satisfiability problem asks if an input exists that will generate a given interval. By excluding data from the language, we achieve PTime complexity for the evaluation problem and satisfiability when only considering inclusive rules, and decidability for the satisfiability problem for cycle-free specifications. Finally, we show that for the full data-free language, satisfiability is undecidable.

Control flow coverage criteria are an important part of the process of qualifying embedded software for safety-critical systems. Criteria such as modified condition/decision coverage (MC/DC) as defined by DO-178B are used by regulators to judge the adequacy of testing and by QA engineers to design tests when full path coverage is impossible. Despite their importance, these coverage criteria are often misunderstood. One problem is that their definitions are typically written in natural language specification documents, making them imprecise. Other works have proposed formal definitions using binary predicate logic, but these definitions are difficult to apply to the analysis of real programs. Control-Flow Graphs (CFGs) are the most common model for analyzing program logic in compilers, and seem to be a good fit for defining and analyzing coverage criteria. However, CFGs discard the explicit concept of a decision, making their use for this task seem impossible. In this paper, we show how to annotate a CFG with decision information inferred from the graph itself. We call this annotated model a Control- Flow Decision Graph (CFDG) and we use it to formally define several common coverage criteria. We have implemented our algorithms in a tool which we show can be applied to automatically annotate CFGs output from popular compilers.

Nfer is a rule-based language for abstracting event streams into a hierarchy of intervals with data. Nfer has multiple implementations and has been applied in the analysis of spacecraft telemetry and autonomous vehicle logs. This work provides the first complexity analysis of nfer evaluation, i.e., the problem of deciding whether a given interval is generated by applying rules. We show that the full nfer language is undecidable and that this depends on both recursion in the rules and an infinite data domain. By restricting either or both of those capabilities, we obtain tight decidability results. We also examine the impact on complexity of exclusive rules and minimality. For the most practical case, which is minimality with finite data, we provide a polynomial-time algorithm.

We present a technique for learning explainable timed automata from passive observations of a black-box function, such as an artificial intelligence system. Our method accepts a single, long, timed word with mixed input and output actions and learns a Mealy machine with one timer. The primary advantage of our approach is that it constructs a symbolic observation tree from a concrete timed word. This symbolic tree is then transformed into a human comprehensible automaton. We provide a prototype implementation and evaluate it by learning the controllers of two systems: a brick-sorter conveyor belt trained with reinforcement learning and a real-world derived smart traffic light controller. We compare different model generators using our symbolic observation tree as their input and achieve the best results using k-tails. In our experiments, we learn smaller and simpler automata than existing passive timed learners while maintaining accuracy.

Nfer is a tool that implements the eponymous language for log analysis and monitoring. Users write rules to calculate new information from an event stream such as a program log either offline or online. In addition to a command-line program, nfer exposes interfaces in Python and R and can generate monitors for embedded systems. Nfer is designed to be fast and has been repeatedly demonstrated to outperform similar tools.

In runtime verification, a monitor is used to return a Boolean verdict on the behavior of a system. We present several examples of the use of monitors to instead document system behavior. In doing so, we demonstrate how runtime verification can be combined with techniques from data science to provide novel forms of program analysis.

We present a Python library for trace analysis named PyContract. PyContract is a shallow internal DSL, in contrast to many trace analysis tools that implement external or deep internal DSLs. The library has been used in a project for analysis of logs from NASA's Europa Clipper mission. We describe our design choices, explain the API via examples, and present an experiment comparing PyContract against other state-of-the-art tools from the research and industrial communities.

In this paper we revisit monitoring real-time systems with respect to properties expressed either in Metric Interval Temporal Logic or as Timed B{\"u}chi Automata. We offer efficient symbolic online monitoring algorithms in a number of settings, exploiting so-called zones well-known from efficient model checking of Timed Automata. The settings considered include new, much simplified treatment of time divergence, monitoring under timing uncertainty, and, extension of monitoring to offer minimum time estimates before conclusive verdicts can be made.

Nfer is a rule-based language for abstracting event streams into a hierarchy of intervals with data. Nfer has multiple implementations and has been applied in the analysis of spacecraft telemetry and autonomous vehicle logs. This work provides the first complexity analysis of nfer evaluation, i.e., the problem of deciding whether a given interval is generated by applying rules. We show that the full nfer language is undecidable and that this depends on both recursion in the rules and an infinite data domain. By restricting either or both of those capabilities, we obtain tight decidability results. We also examine the impact on complexity of exclusive rules and minimality. For the most practical case, which is minimality with finite data, we provide a polynomial time algorithm.

This work describes nfer, an open-source tool for event-stream abstraction and processing. Nfer implements the Runtime Verification logic of the same name, providing programming interfaces in C, R, and Python. Rules that dictate nfer's behavior can be written in an external Domain-Specific Language (DSL), mined from historical traces, or given using an internal DSL in Python. The tool is designed for efficient online monitoring of event streams and can also operate as an offline tool to process completed logs.

This article addresses the question of what properties can be monitored over an unreliable communication channel. We model unreliable communications as mutations to finite traces and define what it means for a property to be immune to such a mutation. We also introduce the idea of a trustworthy verdict, which is a verdict guaranteed to be correct in the presence of a trace mutation. We show that the trustworthiness of a verdict or immunity of a property for a single mutation is equivalent to the trustworthiness or immunity for any number of mutations. We classify trustworthy verdicts on omega-regular properties by updating a recently proposed monitorability-focused refinement of the safety-liveness taxonomy. The article also includes a fixed-parameter tractable algorithm to test an omega-regular property for immunity to a trace mutation. Our results show that many of the most common properties can be monitored over unreliable channels.

In this article, we propose Palisade, a distributed framework for streaming anomaly detection. Palisade is motivated by the need to apply multiple detection algorithms for distinct anomalies in the same scenario. Our solution blends low latency detection with deployment flexibility and ease-of-modification. This work includes a thorough description of the choices made in designing Palisade and the reasons for making those choices. We carefully define symptoms of anomalies that may be detected, and we use this taxonomy in characterizing our work. The article includes two case studies using a variety of anomaly detectors on streaming data to demonstrate the effectiveness of our approach in an embedded setting.

In Runtime Verification (RV), monitoring a program means checking an execution trace of the program for satisfactions and violations of properties. The question of which properties can be effectively monitored over ideal channels has mostly been answered by prior work. However, program monitoring is often deployed for remote systems where communications may be unreliable. In this work, we address the question of what properties are monitorable over an unreliable communication channel. We describe the different types of mutations that may be introduced to an execution trace and examine their effects on program monitoring. We propose a fixed-parameter tractable algorithm for determining the immunity of a finite automaton to a trace mutation and show how it can be used to classify ω-regular properties as monitorable over channels with that mutation.

We propose to demonstrate the open source implementation of nfer (http://nfer.io), a language and system for abstracting event streams. The tool is applicable to a wide variety of cyber-physical systems, and supports both manual and mined specifications. In addition to basic operation, we will demonstrate standalone monitor generation and integration with the popular R and Python languages. The demonstration will use real-world data captured from applications such as an autonomous vehicle and a hexacopter.

We propose a formalism for specifying event stream abstractions for use in spacecraft telemetry processing. Our work is motivated by the need to quickly process streams with millions of events generated by the Curiosity rover on Mars. The approach builds a hierarchy of event abstractions for telemetry visualization and querying to aid human comprehension. Such abstractions can also be used as input to other runtime verification tools. Our notation is inspired by Allen's Temporal Logic, and provides a rule-based declarative way to express event abstractions. We present an algorithm for applying specifications to an event stream and explore modifications to improve the algorithm's asymptotic complexity. The system is implemented in both Scala and C, with the specification language implemented as internal as well as external DSLs. We illustrate the solution with several examples, a performance evaluation, and a real telemetry analysis scenario.

We introduce a novel algorithm for mining temporal intervals from real-time system traces with linear complexity using passive, black-box learning. Our interest is in mining nfer specifications from spacecraft telemetry to improve human and machine comprehension. Nfer is a recently proposed formalism for inferring event stream abstractions with a rule notation based on Allen Logic. The problem of mining Allen's relations from a multivariate interval series is well studied, but little attention has been paid to generating such a series from symbolic time sequences such as system traces. We propose a method to automatically generate an interval series from real-time system traces so that they may be used as inputs to existing algorithms to mine nfer rules. Our algorithm has linear runtime and constant space complexity in the length of the trace and can mine infrequent intervals of arbitrary length from incomplete traces. The paper includes results from case studies using logs from the Curiosity rover on Mars and two other realistic datasets.

In this paper we present a large dataset for use in embedded systems research which has been gathered from a realistic development environment operating in the path of an accelerated neutron beam. The dataset contains traces with events from a real-time operating system as well as user events from a safety critical application. All data is carefully timestamped and in human understandable form. We present two use cases for this dataset: mining timed regular expressions to extract system specifications from clean and possibly anomalous data generated during the operation of the neutron beam, and runtime monitoring to extract information from traces with incomplete information. The dataset is available for research at: http://doi.org/10.5281/zenodo.248008

We propose a notation for specifying event stream abstractions for use in spacecraft telemetry processing. Our work is motivated by the need to quickly process streams with millions of events generated by the Curiosity rover on Mars. The approach builds a hierarchy of event abstractions for telemetry visualization and querying to aid human comprehension. Such abstractions can also be used as input to other runtime verification tools. Our notation is inspired by Allen's Temporal Logic, and provides a rule-based declarative way to express event abstractions. The system is written in Scala, with the specification language implemented as an internal DSL. It is based on parallel executing actors communicating via a publish-subscribe model. We illustrate the solution with several examples, including a real telemetry analysis scenario.

We outline the background, motivation, and requirements of an approach to create abstractions of event streams, which are time-tagged sequences of events generated by an executing software system. Our work is motivated by the need to process event streams with millions of events that are generated by a spacecraft, that must be processed quickly after they are received on the ground. Our approach involves building a tool that adds hierarchical labels to a received event stream. The labels add contextual information to the event stream, and thus make it easier to build tools for visualizing and analyzing telemetry. We describe a notation for writing hierarchical labeling rules; the notation is based on a modification of Allen Temporal Logic, augmented with rule-definitions and features for referring to data in data parameterized events. We illustrate our notation and its use with an example.

Software attestation seeks to verify the authenticity of a system without the aid of trusted hardware, and has important applications in the field of security. Such attestation schemes are of particular interest in the embedded domain, where simplicity and limited resources constrain more complex security solutions. At the same time, these properties enable attestation approaches that rely on predictable side-effects. Most software attestation schemes aim to verify the integrity of memory using a combination of cryptographic schemes, internal side-effects like TLB misses, and known timing constraints. However, little attention has been paid to leveraging non-traditional side-effects, in particular, externally observable side-effects such as power consumption.

In this paper we introduce a method for software attestation using power consumption as the side-effect. We show how to circumvent the undecidable nature of program execution for this purpose and present a static compiler transformation which implements the technique. Our approach is less intrusive than traditional software attestation because the system does not require interruption to compute a cryptographic checksum. It is particularly well suited to real-time systems where consistent timing is more important than speed.

Ensuring correctness and enforcing security are growing concerns given the complexity of modern connected devices and safety-critical systems. A promising approach is non-intrusive runtime monitoring through reconstruction of program execution traces from power consumption measurements. This can be used for verification, validation, debugging, and security purposes.

In this paper, we propose a framework for increasing the effectiveness of power-based program tracing techniques. These systems determine the most likely block of source code that produced an observed power trace (CPU power consumption as a function of time). Our framework maximizes distinguishability between power traces for different code blocks. To this end, we provide a special compiler optimization stage that reorders intermediate representation (IR) and determines the reorderings that lead to power traces with highest distances between each other, thus reducing the probability of misclassification. Our work includes an experimental evaluation, using LLVM for an ARM architecture. Experimental results confirm the effectiveness of our technique.