Tool (Korg), Models (TCP, etc.), and Documentation for Attacker Synthesis Project, with modifications to support RFCNLP paper.
🚨 Changes introduced in this version of KORG have been merged into the official KORG repository. This stand-alone fork exists only to facilitate reproduction of results reported in the RFCNLP paper.
- TOC {:toc}
The documentation for this project consists of this README as well as all the files in docs/
. They natively link to one another so that you can navigate without ever using the file system. These documents are written in Github Markdown and are best viewed online on Github pages, here. We use features of Github flavor Markdown such as emojis, automatic tables of contents, and HTML
.
This repository contains the tool Korg
as well as various Promela models from our paper. The most important parts from the paper are marked with a 📌.
demo/
- contains models used for unit-testing the software, as well as our TCP model.emptyFile
is an empty file used in unit-testing.livenessExample1/
is a small example used in unit-testing. It includes the liveness propertyPhi.pml
.livenessExample2/
is a small example used in unit-testing. It includes the properties: --phi.pml
a liveness property; --theta.pml
the trivial property; and --wrongPhi.pml
a safety property also used in unit-testing. -- the three propertiesphi1.pml
,phi2.pml
,phi3.pml
used in the Case Study forTM_1
,TM_2
,TM_3
.smallDemo1-3
are more small examples with explanations- 📌
TCP/
contains the entire TCP model used in our Case Study.
out/
- this is where the outputs of the program are written to.results/
- this contains the results of the Case Study from the paper. You can reproduce these results using the tool.tests/
- this contains unit-test code forKorg
.__init__.py
- a file needed by Python to handle imports.- 📌
avgExperiment.sh
- a Bash script with which to reproduce our results inresults/
.
📌 The rest of the contents of the repository are exactly the code for the tool Korg
.
Characterize.py
- used to characterize models with respect to properties usingSpin
.CLI.py
- handles basic I/O and CLI aspects of code.Construct.py
- buildsPromela
models.Korg.py
- the main code file for the tool. Drives the rest of the code.Makefile
- a Makefile containing various useful commands for using the tool, and for cleaning up afterword.README
- this README.
From the top-level to run smallDemo1, run the command python3 Korg.py --name=smallDemo1 --dir='demo/smallDemo1/*'
. The output of the demo will appear in out/smallDemo1
. You can change what directory the results appear in by changing the name
flag.
In BibTeX:
@misc{hippel2020automated,
title={Automated Attacker Synthesis for Distributed Protocols},
author={Max von Hippel and Cole Vick and Stavros Tripakis and Cristina Nita-Rotaru},
year={2020},
eprint={2004.01220},
archivePrefix={arXiv},
primaryClass={cs.CR}
}
For more, view the article in Semantic Scholar.
Available here. You can reproduce the results by building the Dockerfile, which will compile and run the code, and compare the results to a saved copy of those from the ArXiV document.
See docs/Korg.md
.