Better Logging Through Formality: Applying Formal Specification Techniques to Improve Audit Logs and Log Consumers
Author
Chapman Flack and Mikhail J. Atallah
Tech report number
CERIAS TR 2000-28
Abstract
We rely on programs that
consume audit logs to do so successfully (a robustness issue)
and form the correct
interpretations of the input (a semantic issue).
The vendor's documentation of the log format is an important part of the
specification for any log consumer.
As a specification, it is subject to improvement using formal specification
techniques.
This work presents a methodology for formalizing and refining the description
of an audit log to improve robustness and semantic accuracy of programs that
use the log.
Ideally applied during design of a new format, the methodology is also
profitably applied to existing log formats.
Its application to Solaris BSM (an existing, commercial format) demonstrated
utility by detecting ambiguities or errors of several types in the
documentation or implementation of BSM logging, and identifying opportunities
to improve the content of the logs.
The products of this work are the methodology itself for use in refining
other log formats and their consumers, and an annotated,
machine-readable grammar for Solaris BSM
that can be used by the community to quickly construct
applications that consume BSM logs.
Booktitle
Recent Advances in Intrusion Detection (RAID 2000)
Publisher
Springer-Verlag
Series
Lecture Notes in Computer Science
Affiliation
Purdue University CERIAS
Publication Date
1900-01-01
Copyright
Springer-Verlag Berlin Heidelberg 2000
Keywords
log, formal, specification, documentation, reliability,interoperability, CIDF, BSM, grammar
