AttackerSynthesis

↞ Back to README.md, ↞ Back to Korg.md

How to use Korg

• How to use Korg
  • As a Tool
    • IO File Grammar / Syntax
  • As a Library

As a Tool

As a tool, Korg should be used through the command line (Bash).

• Yes, it almost certainly works fine in variants such as ZSH. But if you have any difficulties along these lines, feel free to tell us about it in the Issue Tracker, and we will try to help.

The Korg usage is as follows.

python3 Korg.py --model=$1 
		--phi=$2 
		--Q=$3 
		--IO=$4 
		--max_attacks=$5 
		--with_recovery=$6 
		--name=$7 
		--characterize=$8
		--dir=$9

We break down these arguments below. Required parameters are marked with a , while optional parameters are marked with a . Arguments may be given in any order.

• $1 is the system model, e.g., TCP.pml.

  • This is what we call P in the paper.

• $2 is the property the attacker wants to violate, e.g., phi1.pml.

  • This is what we call Φ in the paper, and should be written in linear temporal logic.

• $3 is the vulnerable process that the attacker will replace, e.g., network.pml.

  • This is what we call Q in the paper in the centralized-attacker case, as in, TM = (P, (Q), Φ).
  • In other words, the threat model is TM = ($1, ($3), $2).

• $4 is the IO file.

  • The grammar of this file is outlined in the IO section a little below in this document. Its purpose is to specify what messages the attacker (or Q) can receive or send and over what channels. For example, see IO.txt.

• $5 is the maximum number of attackers Korg should synthesize.

  • Korg can make many many attackers, and often it will generate many very similar or even identical attackers, for subtle reasons having to do with how the trail files are interpreted, so it is a good idea to set this number fairly low until you have a strong grasp of how to best use the tool. I typically like to use --max_attacks=10.

• $6 is True if you want to solve the R∃ASP (that is, the ∃-problem with recovery), or False if you want to solve the ∃ASP (that is, the ∃-problem without recovery). Defaults to False (meaning, EASP).

  • I tend to find attackers with recovery more interesting, but it is generally a good idea to try running it both ways as sometimes attackers with recovery might not exist but attackers without recovery do.

• $7 is the name you want to be used for the folder in out/ where all the outputs will be written.

  • It is usually a good idea to pick something particular to your specific experiment, so you can find your results later on after you have run Korg many times. For some examples, see the names used in our tests. For more documentation on these outputs, see InterpretingOutputs.md.

• $8 is True if you want to have artifacts generated with which to assess the quality and type of your synthesized attackers, or False if you do not want to generate these artifacts. Defaults to False.

  • For more on these artifacts, see InterpretingOutputs.md. Note that setting this to True will slow down Korg, possibly by quite a lot (as in TM_3 in the paper, which corresponds to phi3.pml). I usually tun the experiment with this False first, and then try again with it True.

• $9 is a path to a directory containing phi.pml, P.pml, Q.pml, and IO.txt. If you provide this then you do not need to provide $1, $2, $3, or $4.

IO File Grammar / Syntax

The syntax of the IO file is:

chan1:
	I:a1,a2,...
	O:b1',b2',...
chan2:
	I:c1,c2,...
	O:d1,d2,...
...

In other words, for each channel that the process can communicate over, you have a new line

:

followed by a newline and a tab, then I: and a comma-seperated list of the inputs the process can hear over , followed by a newline and then a tab and then O: and a comma-seperated list of the outputs the process can send over .

We assume that when you provide Korg with an interface, it is the interface of the Q argument, however, we do not computationally enforce this assumption. (Your results might not make sense if this assumption is not met.)

As a Library

Korg can be used as a Python library.

from Korg import *

The best way to see how to do this is to look at the unit tests, e.g., test_Korg.py, which do exactly this.

• If you use Korg in your project, please let us know! We would love to see how you use it.

This site is open source. Improve this page.