Bibtex Entries

@inproceedings{kauffman2019monitorability,
  title = {Monitorability Over Unreliable Channels},
  author = {Kauffman, Sean and Havelund, Klaus and Fischmeister, Sebastian},
  booktitle = {International Conference on Runtime Verification},
  series = {{RV} '19},
  organization = {Springer},
  year = {2019},
  location = {Porto, Portugal},
  pages={256--272},
  numpages={17},
  doi={10.1007/978-3-030-32079-9_15},
  isbn={978-3-030-32079-9},
  abstract = {
    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 $\omega$-regular properties as monitorable
    over channels with that mutation.
  },
  keywords={Monitorability, Unreliable channels, Automata theory}
}
@inproceedings{kauffman2019event,
  author = {Kauffman, Sean and Fischmeister, Sebastian},
  title = {Event Stream Abstraction Using Nfer: Demo Abstract},
  booktitle = {10th International Conference on Cyber-Physical Systems},
  series = {{ICCPS} '19},
  year = {2019},
  isbn = {978-1-4503-6285-6},
  location = {Montreal, Quebec, Canada},
  pages = {332--333},
  numpages = {2},
  doi = {10.1145/3302509.3313327},
  organization = {ACM},
  address = {New York, NY, USA},
  abstract = {
    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.
  },
  keywords = {Event stream processing, Runtime verification, 
              Telemetry comprehension, Temporal logic}
}
@article{kauffman2017inferring,
  author = {Kauffman, Sean and Havelund, Klaus and 
            Joshi, Rajeev and Fischmeister, Sebastian},
  title = {Inferring Event Stream Abstractions},
  journal = {Formal Methods in System Design},
  year = {2018},
  month = {08},
  day = {01},
  volume = {53},
  number = {1},
  pages = {54--82},
  doi = {10.1007/s10703-018-0317-z},
  issn = {1572-8102},
  abstract = {
    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.
  }
}
@inproceedings{kauffman2017mining,
  title = {Mining Temporal Intervals from Real-time System Traces},
  author = {Kauffman, Sean and Fischmeister, Sebastian},
  booktitle = {6th International Workshop on Software Mining},
  series = {{SoftwareMining} '17},
  year = {2017},
  doi = {10.1109/SOFTWAREMINING.2017.8100847},
  month = {11},
  pages = {1--8},
  location = {Champaign, IL, USA},
  abstract = {
    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.
  },
  keywords={Complexity theory, Data mining;Measurement,
            Real-time systems, Software, Telemetry, Tools}
}
@inproceedings{narayan2017system,
  title = {System Call Logs with Natural Random Faults: 
           Experimental Design and Application},
  author = {Narayan, Apurva and
            Kauffman, Sean and
            Morgan, Jack and
            Tchamgoue, Guy Martin and
            Joshi, Yogi and
            Hobbs, Chris and
            Fischmeister, Sebastian},
  booktitle = {The 13th Workshop on Silicon Errors in 
               Logic -- System Effects},
  series = {{SELSE}-13},
  year = {2017},
  location = {Boston, MA, USA},
  abstract = {
    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: 
    \url{http://doi.org/10.5281/zenodo.248008}
  }
}
@inproceedings{kauffman2016nfer,
  title = {nfer--A Notation and System for Inferring Event Stream 
           Abstractions},
  author = {Kauffman, Sean and Havelund, Klaus and Joshi, Rajeev},
  booktitle = {International Conference on Runtime Verification},
  series = {{RV} '16},
  pages = {235--250},
  year = {2016},
  doi = {10.1007/978-3-319-46982-9_15},
  organization = {Springer},
  location = {Madrid, Spain},
  abstract = {
    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.
  }
}
@inproceedings{kauffman2016towards,
  title = {Towards a logic for inferring properties of event streams},
  author = {Kauffman, Sean and Joshi, Rajeev and Havelund, Klaus},
  booktitle = {International Symposium on Leveraging Applications 
               of Formal Methods},
  series = {{ISoLA} 2016},
  pages = {394--399},
  year = {2016},
  doi = {10.1007/978-3-319-47169-3_31},
  organization = {Springer},
  location = {Corfu, Greece},
  abstract = {
    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.
  }
}
@inproceedings{kauffman2016static,
  title = {Static Transformation of Power Consumption for 
           Software Attestation},
  author = {Kauffman, Sean and Moreno, Carlos and 
            Fischmeister, Sebastian},
  booktitle = {22nd International Conference on Embedded 
              and Real-Time Computing Systems and Applications},
  series = {{RTCSA} '16},
  pages = {188--194},
  year = {2016},
  doi = {10.1109/RTCSA.2016.45},
  organization = {IEEE},
  location = {Daegu, South Korea},
  abstract = {
    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.
  }
}
@inproceedings{moreno2016efficient,
  title = {Efficient Program Tracing and Monitoring Through Power 
           Consumption -- With a Little Help From the Compiler},
  author = {Moreno, Carlos and Kauffman, Sean and 
            Fischmeister, Sebastian},
  booktitle = {Design, Automation \& Test in Europe Conference 
               \& Exhibition},
  series = {{DATE} '16},
  pages = {1556--1561},
  year = {2016},
  doi = {10.3850/9783981537079_0829},
  organization = {IEEE},
  location = {Dresden, Germany},
  abstract = {
    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.
  }
}