Runtime monitoring of formal specifications

SpecMon ensures that real-world systems comply with their formal specifications by monitoring applications at runtime. It tracks application behavior through event streams and verifies compliance with the defined rules. SpecMon is lightweight, capable of handling complex scenarios, and supports multiple concurrent sessions.

• Flexible Architecture: Choose your preferred event aggregation method.
• Multi-Session Monitoring: Seamlessly handle multiple concurrent sessions.
• Debugging Made Easy: Quickly identify and fix errors with clear debug output.

• Go 1.21.4+
• Git

1. Clone the repository:

   git clone https://github.com/specmon/specmon.git

2. Navigate to the project directory:

   cd specmon

3. Build the application:

   go build

Note: Detailed documentation and examples will be linked here soon.

$ ./specmon --help
SpecMon is a runtime specification monitor using multiset-rewrite rules

Usage:
specmon [flags]
specmon [command]

Available Commands:
completion  Generate the autocompletion script for the specified shell
help        Help about any command
monitor     monitor the event trace

Flags:
-c, --cpu-profile-path string   cpu profile path
-d, --decompose                 decompose rules (default true)
-h, --help                      help for specmon
-l, --log-level string          log level (default "error")
-m, --mem-profile-path string   memory profile path
-q, --quiet                     quiet output
-r, --role string               role
-s, --spec-path string          specification path
-v, --verbose                   verbose output
   --version                   version for specmon

Use "specmon [command] --help" for more information about a command.

Any contributions you make are greatly appreciated.

For details on how to get started, please see our Contributing Guidelines.

This project is licensed under the GNU Affero General Public License (AGPL) 3.0. See the LICENSE file for details.

If you use SpecMon in your research or projects, please cite it as follows:

@inproceedings{morio2024specmon,
  title={SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols},
  author={Morio, Kevin and K{\"u}nnemann, Robert},
  booktitle={Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security},
  pages={2741--2755},
  year={2024}
}