152 lines
3.4 KiB
TeX
152 lines
3.4 KiB
TeX
%\section{Attacker Model Gadget Examples}%
|
|
%\label{sub:Attacker Model Gadget Examples}
|
|
|
|
\begin{figure}[h]
|
|
\begin{lstlisting}[caption={Example dropping attacker model gadget with drop limit of 3, targetting channel "cn"}, label={lst:korg_drop}]
|
|
chan cn = [8] of { int, int, int };
|
|
|
|
active proctype attacker_drop() {
|
|
int b_0, b_1, b_2;
|
|
byte lim = 3; // drop limit
|
|
MAIN:
|
|
do
|
|
:: cn ? [b_0, b_1, b_2] -> atomic {
|
|
if
|
|
:: lim == 0 -> goto BREAK;
|
|
:: else ->
|
|
cn ? b_0, b_1, b_2; // consume message on the channel
|
|
lim = lim - 1;
|
|
goto MAIN;
|
|
fi
|
|
}
|
|
od
|
|
BREAK:
|
|
}
|
|
\end{lstlisting}
|
|
\end{figure}
|
|
|
|
\begin{figure}[h]
|
|
\begin{lstlisting}[caption={Example replay attacker model gadget with the selected replay limit as 3, targetting channel "cn"}, label={lst:korg_replay}]
|
|
chan cn = [8] of { int, int, int };
|
|
|
|
// local memory for the gadget
|
|
chan gadget_mem = [3] of { int, int, int };
|
|
|
|
active proctype attacker_replay() {
|
|
int b_0, b_1, b_2;
|
|
int i = 3;
|
|
CONSUME:
|
|
do
|
|
// read messages until the limit is passed
|
|
:: cn ? [b_0, b_1, b_2] -> atomic {
|
|
cn ? <b_0, b_1, b_2> -> gadget_mem ! b_0, b_1, b_2;
|
|
i--;
|
|
if
|
|
:: i == 0 -> goto REPLAY;
|
|
:: i != 0 -> goto CONSUME;
|
|
fi
|
|
}
|
|
od
|
|
REPLAY:
|
|
do
|
|
:: atomic {
|
|
// nondeterministically select a random value from the storage buffer
|
|
int am;
|
|
select(am : 0 .. len(gadget_mem)-1);
|
|
do
|
|
:: am != 0 ->
|
|
am = am-1;
|
|
gadget_mem ? b_0, b_1, b_2 -> gadget_mem ! b_0, b_1, b_2;
|
|
:: am == 0 ->
|
|
gadget_mem ? b_0, b_1, b_2 -> cn ! b_0, b_1, b_2;
|
|
break;
|
|
od
|
|
}
|
|
// doesn't need to use all messages on the channel
|
|
:: atomic {gadget_mem ? b_0, b_1, b_2; }
|
|
// once mem has no more messages, we're done
|
|
:: empty(gadget_mem) -> goto BREAK;
|
|
od
|
|
BREAK:
|
|
}
|
|
\end{lstlisting}
|
|
\end{figure}
|
|
|
|
\begin{figure}[h]
|
|
\begin{lstlisting}[caption={Example reordering attacker model gadget with the selected replay limit as 3, targetting channel "cn"}, label={lst:korg_reordering}]
|
|
chan cn = [8] of { int, int, int };
|
|
|
|
chan gadget_mem = [3] of { int, int, int };
|
|
active proctype attacker_reordering() priority 255 {
|
|
byte b_0, b_1, b_2, blocker;
|
|
int i = 3;
|
|
INIT:
|
|
do
|
|
// arbitrarily choose a message to start consuming on
|
|
:: {
|
|
blocker = len(cn);
|
|
do
|
|
:: b != len(c) -> goto INIT;
|
|
od
|
|
}
|
|
:: goto CONSUME;
|
|
od
|
|
CONSUME:
|
|
do
|
|
// consume messages with high priority
|
|
:: c ? [b_0] -> atomic {
|
|
c ? b_0 -> gadget_mem ! b_0;
|
|
i--;
|
|
if
|
|
:: i == 0 -> goto REPLAY;
|
|
:: i != 0 -> goto CONSUME;
|
|
fi
|
|
}
|
|
od
|
|
REPLAY:
|
|
do
|
|
// replay messages back onto the channel, also with priority
|
|
:: atomic {
|
|
int am;
|
|
select(am : 0 .. len(gadget_mem)-1);
|
|
do
|
|
:: am != 0 ->
|
|
am = am-1;
|
|
gadget_mem ? b_0 -> attacker_mem_0 ! b_0;
|
|
:: am == 0 ->
|
|
gadget_mem ? b_0 -> c ! b_0;
|
|
break;
|
|
od
|
|
}
|
|
:: atomic { empty(gadget_mem) -> goto BREAK; }
|
|
od
|
|
BREAK:
|
|
}
|
|
|
|
\end{lstlisting}
|
|
\end{figure}
|
|
|
|
\begin{figure}[h]
|
|
\begin{lstlisting}[caption={Example I/O file targetting channel "cn"}, label={lst:io-file}]
|
|
cn:
|
|
I:
|
|
O:1-1-1, 1-2-3, 3-4-5
|
|
\end{lstlisting}
|
|
|
|
\begin{lstlisting}[caption={Example gadget synthesized from an I/O file targetting the channel "cn"}, label={lst:io-file-synth}]
|
|
chan cn = [8] of { int, int, int };
|
|
|
|
active proctype daisy() {
|
|
INIT:
|
|
do
|
|
:: cn ! 1,1,1;
|
|
:: cn ! 1,2,3;
|
|
:: cn ! 3,4,5;
|
|
:: goto RECOVERY;
|
|
od
|
|
RECOVERY:
|
|
}
|
|
\end{lstlisting}
|
|
\end{figure}
|
|
|