Skip to content

Latest commit

 

History

History
66 lines (41 loc) · 2.71 KB

Korg.md

File metadata and controls

66 lines (41 loc) · 2.71 KB

↞ Back to README.md

Korg is named after the KORG MicroKorg synthesizer, which has a dedicated attack knob (Knob 3). (Source: KORG MicroKorg Owner's Manual, page 9). Image below courtesty of KORG.

  • TOC {:toc}

What is Korg?

Korg is a tool for attacker synthesis. Specifically, given:

  • a system model P, called the "target process";
  • a model Q called the "vulnerable process"
    • with interface IO;
  • and a property phi,
    • where P || Q |= phi,

Korg will try to generate a new process A called an attacker that has the interface IO and violates phi when composed with P.

Intuitively, Korg assumes the adversary can "hack" a process Q in an environment P, and attempts to prove that in so doing, an adversary might induce P to violate phi. The IO is used to stop the adversary from performing actions that Q could never perform in the first place.

How can I install Korg?

See the install docs.

How can I use Korg?

See the usage docs.

... using the Makefile

Read the #comments in the Makefile. TL;DR:

  • To run experiment1 without recovery, do make experiment1.
  • To run experiment2 or experiment3, change --phi=demo/TCP/phi1.pml to --phi=demo/TCP/phi2.pml or --phi=demo/TCP/phi3.pml in the experiment1 target. Then do make experiment1.
  • To run experiment1 with recovery, change --with_recovery=False to --with_recovery=True in the experiment1 target, then do make experiment1.
  • To reproduce our results, do make avgExperiment.
  • To run unit tests for main body of Korg logic, do make testKorg.
  • To run unit tests for Characterize.py, do make testChar.
  • To run unit tests for Construct.py, do make testCons.
  • To run all the unit tests, do make test.
  • To clean up after running one of the targets, do make clean.

... using Bash

See the Usage docs, or, adapt the commands in the Makefile to your needs.

... using Windows

Use Cygwin, or, a virtual machine, or, the Linux Subsystem.

  • Please use the Issue Tracker to report any issues. We have not yet tested on Windows.

I ran Korg on my threat model. Now, how do I interpret the results?

See interpreting outputs.

Help! It's not working!

See troubleshooting.