Publications

[9] Sean Kauffman, Klaus Havelund, and Sebastian Fischmeister. Monitorability Over Unreliable Channels. In International Conference on Runtime Verification, pages 256 - 272. Springer, 2019. [ bib ] [ pdf ]

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.

[8] Sean Kauffman and Sebastian Fischmeister. Event Stream Abstraction Using Nfer: Demo Abstract. In 10th International Conference on Cyber-Physical Systems, pages 332 - 333. IEEE/ACM, 2019. [ bib ] [ pdf ]
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.

[7] Sean Kauffman, Klaus Havelund, Rajeev Joshi, and Sebastian Fischmeister. Inferring event stream abstractions. Formal Methods in System Design, pages 54 - 82. Springer, Aug 1, 2018. [ bib ] [ pdf ]
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.

[6] Sean Kauffman and Sebastian Fischmeister. Mining temporal intervals from real-time system traces. In 6th International Workshop on Software Mining, pages 1-8. IEEE, 2017. [ bib ] [ pdf ]

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.

[5] Apurva Narayan, Sean Kauffman, Jack Morgan, Guy Martin Tchamgoue, Yogi Joshi, Chris Hobbs, and Sebastian Fischmeister. System Call Logs with Natural Random Faults: Experimental Design and Application. In SELSE-13: The 13th Workshop on Silicon Errors in Logic — System Effects, Boston, MA, USA, 2017. [ bib ] [ pdf ]

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

[4] Sean Kauffman, Klaus Havelund, and Rajeev Joshi. nfer — a notation and system for inferring event stream abstractions. In International Conference on Runtime Verification, pages 235 - 250. Springer, 2016. [ bib ] [ pdf ]

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.

[3] Sean Kauffman, Rajeev Joshi, and Klaus Havelund. Towards a logic for inferring properties of event streams. In International Symposium on Leveraging Applications of Formal Methods, pages 394 - 399. Springer, 2016. [ bib ] [ pdf ]

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.

[2] Kauffman, Sean and Moreno, Carlos and Fischmeister, Sebastian. Static transformation of power consumption for software attestation. In Embedded and Real-Time Computing Systems and Applications (RTCSA), 2016 IEEE 22nd International Conference on, pages 188 - 194. IEEE, 2016. [ bib ] [ pdf ]

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.

[1] Moreno, Carlos and Kauffman, Sean and Fischmeister, Sebastian. Efficient program tracing and monitoring through power consumption — with a little help from the compiler. In 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 1556 - 1561. IEEE, 2016. [ bib ] [ pdf ]

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.