From 9b0f340c0be9b8fd79e5a33543c7215ce20bd167 Mon Sep 17 00:00:00 2001 From: Jake Ginesin Date: Mon, 27 Oct 2025 01:14:12 -0400 Subject: [PATCH] init - first working version --- README.md | 15 + flake.lock | 61 +++ flake.nix | 34 +- .../model_generate.cpython-313.pyc | Bin 0 -> 16533 bytes src/__pycache__/utility.cpython-313.pyc | Bin 0 -> 7113 bytes src/main.py | 146 ++++++++ src/model_generate.py | 346 ++++++++++++++++++ src/utility.py | 168 +++++++++ test_harness.py | 65 ++++ tests/drop/t1-drop.pml | 20 + tests/drop/t2-drop.pml | 22 ++ tests/drop/t3-drop.pml | 22 ++ tests/drop/t4-drop.pml | 24 ++ tests/drop/t5-drop-multi.pml | 24 ++ tests/drop/t6-drop-overwhelm.pml | 24 ++ tests/reorder/t1-reorder.pml | 30 ++ tests/reorder/t2-reorder.pml | 36 ++ tests/reorder/t3-reorder.pml | 36 ++ tests/reorder/t4-reorder.pml | 34 ++ tests/replay/3-jump.pml | 29 ++ tests/replay/replay-out-of-order.pml | 34 ++ tests/replay/t1-replay.pml | 24 ++ tests/replay/t2-replay.pml | 19 + tests/tests.yaml | 76 ++++ 24 files changed, 1277 insertions(+), 12 deletions(-) create mode 100644 README.md create mode 100644 flake.lock create mode 100644 src/__pycache__/model_generate.cpython-313.pyc create mode 100644 src/__pycache__/utility.cpython-313.pyc create mode 100644 src/main.py create mode 100644 src/model_generate.py create mode 100644 src/utility.py create mode 100644 test_harness.py create mode 100644 tests/drop/t1-drop.pml create mode 100644 tests/drop/t2-drop.pml create mode 100644 tests/drop/t3-drop.pml create mode 100644 tests/drop/t4-drop.pml create mode 100644 tests/drop/t5-drop-multi.pml create mode 100644 tests/drop/t6-drop-overwhelm.pml create mode 100644 tests/reorder/t1-reorder.pml create mode 100644 tests/reorder/t2-reorder.pml create mode 100644 tests/reorder/t3-reorder.pml create mode 100644 tests/reorder/t4-reorder.pml create mode 100644 tests/replay/3-jump.pml create mode 100644 tests/replay/replay-out-of-order.pml create mode 100644 tests/replay/t1-replay.pml create mode 100644 tests/replay/t2-replay.pml create mode 100644 tests/tests.yaml diff --git a/README.md b/README.md new file mode 100644 index 0000000..3282899 --- /dev/null +++ b/README.md @@ -0,0 +1,15 @@ +# Korg, reborn + +# TODO: +- [x] fix weird spin errors(?) +- [ ] add attackers that only do specifically n queries + - limitation: you cannot choose only *n* queries for the dropping attacker +- [ ] add attackers to do <= n queries +- [x] add a test suite +- [ ] modify the paper? spin workshop? +- [x] nix flake here lol + +# Notes +- Sound and complete attack discovery for replay, dropping, and reordering attacks on channels + - possible because of the finite-state modeling spin does +- Limiting the number of messages a drop/replay/reorder attacker can reason about has the ability to significantly reduce the searchspace, especially when dealing with larger models. Although KORG is always decidable, sound, and complete, using the unbounded attacker is inadvisable in practice because spin must reason about *all* such permutations of possible drop, replay, and reorder sequences, thereby increasing the search space factorially. diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..1f39180 --- /dev/null +++ b/flake.lock @@ -0,0 +1,61 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1761373498, + "narHash": "sha256-Q/uhWNvd7V7k1H1ZPMy/vkx3F8C13ZcdrKjO7Jv7v0c=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "6a08e6bb4e46ff7fcbb53d409b253f6bad8a28ce", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix index 4512e49..6fc6ddf 100644 --- a/flake.nix +++ b/flake.nix @@ -2,28 +2,38 @@ description = "korg flake"; inputs = { - nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; + nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; flake-utils.url = "github:numtide/flake-utils"; - nixpkgs-spin.url = "github:NixOS/nixpkgs/893c51bda8b7502b43842f137258d0128097d7ea"; }; - outputs = { self, nixpkgs, flake-utils, nixpkgs-spin, ... } @ inputs: + outputs = { self, nixpkgs, flake-utils, ... }@inputs: flake-utils.lib.eachDefaultSystem (system: let pkgs = nixpkgs.legacyPackages.${system}; - pkgs-spin = nixpkgs-spin.legacyPackages.${system}; - in { + + pkgs-spin = import (builtins.fetchTarball { + url = "https://github.com/NixOS/nixpkgs/archive/893c51bda8b7502b43842f137258d0128097d7ea.tar.gz"; + sha256 = "0wydvj05k9cjx557gvr1am7rzl482zv9ml0p3zamxm1gx7whzja6"; + }) { inherit system; }; + + spinPkg = pkgs-spin.spin; + + in + { packages.default = pkgs.stdenv.mkDerivation { - pname = "korg"; - src = ./.; + pname = "korg"; + src = self; + installPhase = '' + mkdir -p $out/bin + echo "placeholder" > $out/bin/korg + ''; }; devShells.default = pkgs.mkShellNoCC rec { - buildInputs = with pkgs; [ - # spin - python3 - ] ++ [ - pkgs-spin.spin + buildInputs = [ + pkgs.python3 + spinPkg + pkgs.python313Packages.pyyaml ]; shellHook = '' diff --git a/src/__pycache__/model_generate.cpython-313.pyc b/src/__pycache__/model_generate.cpython-313.pyc new file mode 100644 index 0000000000000000000000000000000000000000..a2c4aff8dd3d4e06e7feeaf1106e9ee2de237664 GIT binary patch literal 16533 zcmeG@TTC2Rmet+W51Lms4`ci+9>#!;8;oB(Z1XS^8$aSu;DBR?K-0!JrW;i^iE%a= zOFPnL=4U;ctYpdlAnSZ!*&js72U7CEPDUf7nUA_6QmodjcBK8vA6a{(+5XtwbMEcF zb#JTN;KVygcGD84PThO%x#yl+)IG0yQdsC$;P;Ea{@2yzW<~jTyh;CP58OOa9g6Z# zilG>e(~8Ni4%0#Jou-psU8aj(Ra1ql^R&C)V|sMOa9#2m>Lt%5uNxQ{?n^$y1ApF2 z-UEKaw?(<8nt2&C>3*M)NBjL5{W1?frOD5rv3cav{(_8tnMVPoDa@d;c@)zAqDeQM7*D3X?l*TReJJS7z$MC8O?e`%Zz*#eX zMxNm~=wywQ(vPsIP*JE<`5Y?{W{~A8v_}M$h}$TNc!nIM%E@EE!#m_2z+KPy8N~uO zPg-8&lg4#rNEK+j>2^ays^JUB6fr}T*JF67yq>dNijuGBqSoA{$^~!C8B}6UkPY@D z`u2I}S=a%ji#a3q3{-3D=_=xbJqrjD%DW;;r5Yt%i=`YZ<5;=Cg|DBkZ4*MF*O%4; z?X5t_xoj5bWGl0CWX>Zp-lH(vr(Ph2q81RlxPlbS6 z(xvOHt20@0jCG0PyYwnOnFlobR8tdh_fqtVKe+=DU<;EU)thnPWHcVt2l~#R=^g>X zoxHzF>`w`o=5%GspY$N*yZ&SWUdLfA*Ta$eq^luKgG13#~v1yp64%x@T*TbQB{n)hL4h!11kIo}+rl+B)1?4J9i37B$ z)%lYFY}0`stYB=qsRhVNQ%%wX;eu@dV!8>UrUjlUjrw8BfGkRuu{UvYd*xi) zTcqX5LaQC9-OZFDJUtVitC#x&Hou;MzV6d7g_k0rHs`zk2d;!G7B>@K`WS}73D4Nf zOgJ*}AkRe8$;9K{gu_}f(Rxbw!K@ku`l-ld!Z#I%e}OU6O!z4liq1yBDnmTsyb_D$ z!2q^4fQioF)#!9M7@LcPuA0$EbT$?YMJK|+H>2icaLkNdAB!|a!fyv-W+*rf9oI)E z!;!E#77y>6nM?TLW|aM>nCF2n$`%_2cuRR4D81GHXSK)*?D{CQu_~cH6F4iu2{w-IWuWpi;y#suTI|}r*Bwue`me> z^CyaO#?kHkMo~(-ookA6!g-3`Q0PA8yw(3$ExKJs)biA{t)KQTxj*SAfn!TINZ=)+ zz62e`fmA!NR0lMKJ={?HT<*hj{2+khdxr& zuB7Ln3ZgYzEj>i*A!-jJbAJ%JQ~R5#Ul-4N zh*mdm!UR_1F`^y&JhpuBvztUawX%z7FI(pah&Esu!$cb<>Tu??Tog-dA!-ZlwzU03 z-Ong_|Lr`YRYF(Ip*iN*A)}ek_BT@U=I{20eD{`}c=KOL? zE&tE|7(1gOs^BGhBroxb$Gsf>H!!2+9#`LV*69S%F|Pf-MNPBG`stJAxeub|TObR3WHF zP=jDEfMgjO(%>P_>1K!5IW+5u5`M z^8vv1;Lm&+ZW3j-(LXvH83*@bB0OPUfUck6fU?}?|8_9Omuvr6x-#;I9oF!Ob@7sQ z>N4rMY`rl-dM3W=j*#w%6*aBc>}vO0B=D9s_Z|tnN7VP2jqsx|?!Rv%o?B*?wwtKC zQ+8K9QR|r!dB0#o|75!VWV-)vn(lB2q)qpR{L>A-?CGDSwCVnTF8w2=ccfrA7{uw+ zkS|ASNE41wZf@hbAsGFlBg2y-U|s{&w@eNBB%}X*$>_Id*jQ>P4^l%V!YX9rK~Ah> zO$bp#0H2C=%z9ytytH;u2h7mtTq*@Ru0={m(?Oh$8TUBvwwxoj<2XKIqbZMa|ja1Ypazc5R*KzgG7@&Il0KYV2AweV7#69$(rur>#&nXO}s5@YKQl>2vW&1 z)5H#^v(q&Pc$=MCIh2#jv-Nj4L%XsB&!e>?T&fo(i~Mvxk1TCmmUfQWX~~Y9y6Tjk zrlWl9F^(NiW85tFfmz-qnB`^xJg;UUg7t0kWYsfLFi~>?QaZ^1pVQmg zcs{03im40cd?n6}Hht1_>fEV8h^f0Ep<$c#NiR*vyhBqIXxXMSAk->nsTY>Up$P(N zF8my0Dx27-+sjfa@@V35aLsQFK4`Em%?r%zWxk zP|t!o73jEttA$HqsSM^)P>)6SD;oTQU%}H88O}wbK-@OL)j+=v7r=hZ*~n+k27M6B z2oU@O{Kfv_`az@^4t#1Xm49-P1ddx>gCsCW)Il-F@aNL%kBo)#`xi-R@Yb2{DdT`y zk@YhUb{OA7)J?Dm7?sN_ScJfN2T?mxu7&HOe*2v|2R93pnQ;5JWUSXwQpq3k|{ zu=iO(DU8f%Y-hyM>WEs$d=(}OuD~X=+XVR_rLp^wYoX_%7g7pVa~A}jiQ1K7@53fj z|Ep;y0wa844Vi3oy6~9$p~e3VF}^R!D^-wX&kcwbWE;s1a5E=WLH6x(0~@O#+gNVE z2RoKEBR~xf+|M$>Y>`bP8vPe~xr;*gnbwVQE)@cu%!TFyI9(;jw&WZ^YkoN0vvUB< z{K9pxsxZWuyYuX|RpA;03FNiOar_#API49v>Lv)iG8Z|&ku|o@SIJxgl-Z8n+iMfz z_=|&LH z82m-VG6M0hVcR7Hb|C&T-oB222F^zjdjr83f^h^iwjM%k0s%L*%`o0xK|t+mw1Q0o z!5{(}m!Cw8hTpkmZC=H;DFieIe+@AjgMSmT3?unEw$V^~HoI6X+sPJhpT^N=5zwH! zRHMTT;c~$c7Q*f`FlGh*Vjt%=iCw^EKbfsW{xo<6nCE$O(3?8w1Qb98+o$)TLn6K&D(H)xdhCBzi}-% zjnBoyv~W8W8$8>6>Rh`&Ysw$PZ#TDNBnqNl8Rgcgg58_NsqXOgSQvtNev{e-7~H#= z3LDbNrt~Hq3zO4rv{(SA?(oyFUS>@IHBV5XNg>dfqNkxaD0)su7gM6J>VaMuLv#EO zT;|UZKZ)Qa1g8MRvRD;9v?@@G<_)0mIxv3^uN<*_x8>8C#qcMMB+$7uOagsG?Yq^# z=25hgbS16td#j|)zt=nOx_gpnwev#|3?XVG3nuU*PdNVV0D}-W!b;kO5~A&~Xc&g5 zM>7~$S~F3bQ?ZR|qE@G(6%c_LybCd}>UjvjFcu4aLi9^2Ahn|`*#yfFCs$$bbJopD zA+RjdO7SFKWNZ_HO`#)aUmd&JlX~efq3Ihhd%23w^t|XyK!pQTPaUZ064p z&#H|CH~4u5AHV@Kq43duUcJUZLD9l;xcnd*>^Z7Qm4FSkf$5oPk_Y3ai zO(1Q>Q{Wo_&vgoXkKa>darU0;ZO=pYQoQ}!z3qkabvvi>V|c~4h_Cn^zJ_A>0BJ6k zaGK$SKQ=p#AIODca375&Jh7{@@u}+x4}38PUmThE#-;{G!UdT~`XLZ42c-Er6C)JV zx-jwKdZ0W3sIZuZuM<8gn!O%AX8r=&;E7XW#Q@h_4u|94l)A5!x>cp_UzLhAwaeky zbUU=B;B`K}(EH&W!c@K5n2WP7N(MGhEi*b2I`= zmdP|q#n_e;OQ{@NAGTy!AK`|s6v@_6gEqSxc zSW*xi+rt5LdTM~=Kbc)XvbzVBPf6K!~a_Pk1B+IPhPa5FFfp|;NeZg zBc2*XIL|3esqZwVRnA~Wbc_LWiJjRArVwm(A|hqe0W8YFc?SvBFbOV^M2tyK1azjh(miHucG|NVy%KlitSN zl)_#NNwQ*G2!(}l|FWRyu^`8=7@!L75Jtv=f#1##fV_zg!zhTuYxNc)(2v_LhW8CElDKz`_h z=q%C;1^Fg3u25J(Zbo4vQ9)EpSnvnKAyJSN)6hylh{~aexXEB*MPcL>S)muOM118q zPC4mWiYyBrX;lm?;fNTCNuEF?D0p6q;6;xgOJTp*DGFCT5)OD`awr^Jt{M(j%$fy7ac*3;H)qcz@?HCPhE>w!-Uhm!N#Cd-Z5Yqi%8$4`90AY;va zlQrJo(Xx-V)ykqJ^@0oiI|HSs8e_{I2 z&&+4d%smqY^#9|`VFP@do53U;6_(5zw!$N}0nz3Mml2`5P|0Xx7rd(SuN&y9YgN~) z{|5t&%SlJNWtjW${)4H&0(}!b1wjBm+J`F8@O^|t#>aR;vbR8R6l%2v?(auvrVua) zd5ep>)Upv^#K&kMBC<1NfYjn+y(aCs#Cb;RL*rA;`|7cpycHTh#$TPLQ}j3T4gA&b z_V+Pf7JGk;y!aJfOX=IRC*HstwGr`>ncq`*lje6+m~m*r84{3c@#!_W#;06l6vpnu z@81!!0Gtr8aht~<8JdE^0>ty9=Gns2tkiaN=4|JS{?4`8x!KOk?QXT^sm`9u?$60w zeoiJ?VFOEkag8HXm4iAoDzxZon|3agk_?g2D#bl7-C(9-G%=X%@O;4jv-v0H z50Cw$Ez@y2G5&V%TfH0p+kI)PTWkFEmZdRmY5YuUeCBR*rs8~JFsDZ~^>4Sm)wc2c z?an)u?;qMc^ugKp>bBgc)9%wBN_UTE+~>C37t`*Gzv46Q=hs`ZbqzmixubixBU9%| z3|}9AP>aeAJ~)P)2XfuWS{a|%fp0)xiD~lvWCPe)fjKP2G{iNd#`T{du31>Ef62IJ zwN)(YcEz=B-*_!XL~+fY+*hv{S!!JG@9&?-b>bVvb;)17PhZ3YFW`s%$-X>BUi_xV z$PL=J?u!COi1Pw=?u!Cut#vdh8Ybwm-y=v^c8#-9lZ(cwn?3^>uc`0l`54Uh*q3=E zm@4n4Nm?>v2L-i2%5j9G9J>&uXlsV-8EWaBLdXwW)zsfU3-3W#UsZ^=XvvR2O`Xy~ zy=bgQ<7c$Q#cdtO2cZ^M6LN@<8bWG;to0PJq=Y^MbpS?YG(>`T4U{gIK<0C@uyGwB z1Z(hNVlME?@?79$e>f(*%7rAcRp#GaTa>cyGN&}`~Tc*Z@651HR2s=jbm8yGTFCGmwqZlX=`d^2YLdY9t}KGmWCAD@W+SMsPga*VxVb7Rnqvz z=^yc#ilf^#O_`dL(2?shaplxy(i=RdYEEv~cc$x~Ss(sW&H#-bNhDBy(P=s_k0j$st!MaaXz@dNDSi?@IV+B@Nmu#@l7*eAn! zvXp0f81*1S_J=)1i{%*f8||JkYGN;0WqZng2<1aX1k&wlUBsD^iPE7^gzU;&%w$R$ znlG?hu}_qaZ|A6Hlj5`{-}r+<@%{6h{#VzSBwj1?V_2wv-w zmjn!eAPCD6Cr7w>f%9{4T$24OoT|ZvL=JQ~buJs!#3nW$#gTv@Ns4Y#J(IDMBa=gl zB@kI&j)|dwUltTPA}K7HdBr&ImjpG4^^1ZWxEfUSL4h2?Aj5eUzFJ`d%R$fullTn0 zTlrlHR2eKB| zmZj!nOHFd%$L9APn~smnzjWMlq%D*2!EIOdma8T0YRR}-zdIg3mvuOAT)lR6%Tb?p z)NhzGj`sL))?Ria^jhfpOY!rN!PqNrT)uYs`ds|nwymQ0Xemz~$ym4)>rFL!Gpsjl z;jjlh`O4ZSD~mw*&QF2n*FMj{JR*D`?Xa? zawguO?u8KW(0-qMUele2RXI`RV~d#uM8Z^eCuH~{GgHj-i9O!fLvv_s1R>r8s~H?Q zPx%41OImz!_lJGD7*XCb&F2!|6l22l$=&_|X4-iN zU-o~pZkz?&B$>>fqRqF8n=89!ha^0EikD<9d&(}{H0^5r?xWrqQPf; zqTE$&;mftvLUi2~Kny|s`93zOqHFMN2_HtKoL>AT>{Icv1yu`^E&Vt-RBqjzMpm0$P zXGJ*aHJBC3v!?F?c__TbdZ6hV(W+lxKp{Xh*CCYip#OBTd!zQwTFTrTANXv4;7?t8 zF>RTN58gLh;{)4f`?k|{tLA3Sma`@8Y{@uV6MC|Hc&~peIr#R-TO+qe)3qnItA~B6;a8%f^eTr-nZ`v~{dMeXRfPiOjL{sg{vnolCcPe{JROJ1cJ1Z=6ay+Y|jc zBPu(v9!mx{2Jf_`>?adU)=>@H*~hS*F+aZW{>0|QM;CrMac?5+cma<4)pc9d?sT;~ zQ{8^ep3sx?{xdh9*{WztS2S&0$W(X|#%y`zE%)p0H`)^h*#627-m1G<_eMPolCw&C z{LE-eEc}BF*xwt}F&O!^@j`z8gV`yTV(xburt3}Qf$Z;jN(4lN`?kLZ@55D3Z9JGavhU{uzcLN9aSp`cF*~L7N*ZCMbIzg9YV{jxPcSmEe zWWRycq9=Q-QhTgQd8>;ooIyz@pcXiTLM}_Ly~hN&Brjcz@2Bzol7?HqcGxQ{M|!`Fui^svPXloXe;c$E!vwFM1l_FSP(7TJ zBXfBL#Q?dXEMO6n*j1!*Kft%7v!*7VKk5mWX=wLnE z-aD(6%7buw@2vjvp%qouK$XpC?UwH3Q ts=50idC#4p%oI;;fEB{;un$$9tMyQ$6lp{F#^6Jh|K~haNx4+#{~NXhai0JH literal 0 HcmV?d00001 diff --git a/src/main.py b/src/main.py new file mode 100644 index 0000000..75c5d5b --- /dev/null +++ b/src/main.py @@ -0,0 +1,146 @@ +# ============================================================================== +# Author : Jake Ginesin +# Authored : 14 June 2024 +# Purpose : synthesize attacker gadgets for attackers that can drop, +# replay, and reorder messages on a channel +# ============================================================================== +import sys, re, subprocess, os, shutil +from typing import List + +from utility import * +from model_generate import * + +def show_help() -> None: + msg=( + "Usage: \n" + " python main.py [arguments] \n\n" + "Arguments: \n" + " --model=path/to/model.pml Promela model to generate attackers on\n" + " --attacker=[replay,drop,reorder] \n" + " --chan=[chan1, chan2:int, ...] Channels to synthesize attackers on. When specifying over ranges of\n" + " channels, you can give ranges or a list of values\n" + " --nocheck Don't check channel validity\n" + # " --nchan=[nat, nat, ...] If the channel is a set of channels, how many attackers to synthesize?\n" + " --mem=[num] Size of memory. Defaults to '3' \n" + " --mem=unbounded Use the unbounded memory gadget version (not recommended)\n" + " --output=path/to/file.pml Outputted file name\n" + " --eval Evaluate the outputted file with Spin\n" + " --cleanup Clean up the extra files spin creates, including Korg's \n" + ) + print(msg) + + # assert "syntax error" not in stdout, "there seems to be a syntax error in the model" + # assert "processes created" in stdout, "the spin model creates no processes ... check to see if it compiles" + +def main() -> None: + args = sys.argv[1:] + if len(args) == 0 or args[0] in ["help", "--help", "-h", "-help"]: + show_help() + sys.exit() + + mem = 3 # default + + for arg in args: + if arg.startswith("--model="): + model_path = arg.split("=", 1)[1] + elif arg.startswith("--attacker="): + attacker = arg.split("=", 1)[1] + elif arg.startswith("--mem="): + mem_read = arg.split("=", 1)[1] + elif arg.startswith("--chan="): + chans = arg.split("=", 1)[1] + elif arg.startswith("--output="): + out_file = arg.split("=", 1)[1] + + if "--eval" in args and not "--output" in args: + out_file = "korg-promela-out.pml" + + if not model_path or not attacker or not mem or not chans or not out_file: + print("error: all arguments are required. \n") + show_help() + sys.exit(1) + + unbounded = mem_read == "unbounded" + if not unbounded : mem = int(mem_read) + + ensure_compile(model_path) + model = fileRead(model_path) + + channels = parse_channels(fileReadLines(model_path)) + mchannels, mchannel_len = parse_mchannels(fileReadLines(model_path)) + model_with_attacker = str; + assert mem >= 0, "memory value must be positive" + + chans_togen = set() + + # first, process the input + mc = chans.split(",") + for chan in mc: + if ":" in chan: + name, num_extr = chan[:chan.index(":")], chan[chan.index(":")+1:] + if "-" in num_extr: + a, b = list(map(lambda a: int(a), num_extr.split("-"))) + assert a < b + assert a >= 0 + assert b < mchannel_len[name] + for i in range(a,b+1): + chan_name = str(name) + "[" + str(i) + "]" + chans_togen.add(chan_name) + channels[chan_name] = mchannels[name] + else: + a = int(num_extr) + assert a >= 0 + assert a < mchannel_len[name] + chan_name = str(name) + "[" + str(a) + "]" + chans_togen.add(chan_name) + channels[chan_name] = mchannels[name] + + else : chans_togen.add(chan) + + print(chans_togen) + + for i in range(len(chans_togen)): + chan = list(chans_togen)[i] + + if not "--nocheck" : assert chan in channels, "can't find "+str(chan)+" in model" + + match attacker: + case "replay": + if unbounded : attacker_gadget = gen_replay_unbounded(chan, channels[chan], i) + else : attacker_gadget = gen_replay(chan, channels[chan], mem, i) + case "drop": + if unbounded : attacker_gadget = gen_drop_unbounded(chan, channels[chan], i) + else : attacker_gadget = gen_drop(chan, channels[chan], mem, i) + case "reorder": + if unbounded : attacker_gadget = gen_reorder_unbounded(chan, channels[chan], i) + else : attacker_gadget = gen_reorder(chan, channels[chan], mem, i) + case _: + print("error: inputted an invalid attacker model. \n") + sys.exit(1) + + if model.rindex("};") >= model.rindex("}"): + model = model[:model.rindex("};")+2] + "\n\n" + attacker_gadget + "\n" + model[model.rindex("};")+2:] + else: + model = model[:model.rindex("}")+1] + "\n\n" + attacker_gadget + "\n" + model[model.rindex("}")+1:] + + # Write the modified model to the output file + with open(out_file, 'w') as file: + file.write(model) + + if "--eval" in args: + print() + print("generated Promela file with attacker model gadget... now running SPIN on "+str(out_file) + "!\n") + eval_model(out_file) + + if "--cleanup" in args: + print("\nCleaning up Spin files...") + cleanup_spin_files() + try: + os.remove(out_file) + print(f"Removed: {out_file}") + except OSError: + pass + + +if __name__== "__main__": + main() diff --git a/src/model_generate.py b/src/model_generate.py new file mode 100644 index 0000000..2f3dd4c --- /dev/null +++ b/src/model_generate.py @@ -0,0 +1,346 @@ +import sys, re, subprocess, os, shutil +from typing import List + +def gen_replay(chan : str, chan_type : List[str], mem : int, index : int) -> str: + ret_string = "" + + ret_string+= "chan attacker_mem_"+str(index)+" = ["+str(mem)+"] of " + ("{ " + str(chan_type)[1:-1] + " }") .replace("'","") + ";\n" + ret_string+= "\n" + + ret_string+= "active proctype attacker_replay_"+str(index)+"() {\n" + + item_arr = [] + item_count = 0 + + # formulate string of general message input variables + for item in chan_type: + item_arr.append("b_" + str(item_count)) + ret_string+= str(item) + " " + item_arr[item_count] + ";\n" + item_count+=1 + + fs = (str([item for item in item_arr])[1:-1]).replace("'","") + + ret_string+="int i = "+str(mem)+";\n" + ret_string+="int b;\n" + ret_string+="CONSUME:\n" + ret_string+=" do\n" + ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n" + ret_string+=" "+str(chan)+" ? <"+fs+"> -> attacker_mem_"+str(index)+" ! "+fs+";\n" + ret_string+=" i--;\n" + ret_string+=" if\n" + ret_string+=" :: i == 0 -> goto REPLAY;\n" + ret_string+=" :: i != 0 -> goto CONSUME;\n" + ret_string+=" fi\n" + ret_string+=" }\n" + ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n" + ret_string+=" b = len("+str(chan)+");\n" + ret_string+=" do\n" + ret_string+=" :: b != len("+str(chan)+") -> goto CONSUME;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" od\n" + ret_string+="REPLAY:\n" + ret_string+=" do\n" + ret_string+=" :: atomic {\n" + ret_string+=" int am;\n" + ret_string+=" select(am : 0 .. len(attacker_mem_"+str(index)+")-1);\n" + ret_string+=" do\n" + ret_string+=" :: am != 0 ->\n" + ret_string+=" am = am-1;\n" + ret_string+=" attacker_mem_"+str(index)+" ? "+fs+" -> attacker_mem_"+str(index)+" ! "+fs+";\n" + ret_string+=" :: am == 0 ->\n" + ret_string+=" attacker_mem_"+str(index)+" ? "+fs+" -> "+str(chan)+" ! "+fs+";\n" + ret_string+=" break;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n" + ret_string+=" b = len("+str(chan)+");\n" + ret_string+=" do\n" + ret_string+=" :: b != len("+str(chan)+") -> goto REPLAY;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: atomic {attacker_mem_"+str(index)+" ? "+fs+"; }\n" + ret_string+=" :: empty(attacker_mem_"+str(index)+") -> goto BREAK;\n" + ret_string+=" od\n" + ret_string+="BREAK:\n" + ret_string+="}\n" + + return ret_string + +def gen_replay_unbounded(chan : str, chan_type : List[str], index : int) -> str: + ret_string = "" + + ret_string+= "chan attacker_mem_"+str(index)+" = [99] of " + ("{ " + str(chan_type)[1:-1] + " }") .replace("'","") + ";\n" + ret_string+= "\n" + + ret_string+= "active proctype attacker_replay_"+str(index)+"() {\n" + + item_arr = [] + item_count = 0 + + # formulate string of general message input variables + for item in chan_type: + item_arr.append("b_" + str(item_count)) + ret_string+= str(item) + " " + item_arr[item_count] + ";\n" + item_count+=1 + + fs = (str([item for item in item_arr])[1:-1]).replace("'","") + + ret_string+="int b;\n" + ret_string+="CONSUME:\n" + ret_string+=" do\n" + ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n" + ret_string+=" "+str(chan)+" ? <"+fs+"> -> attacker_mem_"+str(index)+" ! "+fs+";\n" + ret_string+=" do\n" + ret_string+=" :: goto REPLAY;\n" + ret_string+=" :: goto CONSUME;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n" + ret_string+=" b = len("+str(chan)+");\n" + ret_string+=" do\n" + ret_string+=" :: b != len("+str(chan)+") -> goto CONSUME;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" od\n" + ret_string+="REPLAY:\n" + ret_string+=" do\n" + ret_string+=" :: atomic {\n" + ret_string+=" int am;\n" + ret_string+=" select(am : 0 .. len(attacker_mem_"+str(index)+")-1);\n" + ret_string+=" do\n" + ret_string+=" :: am != 0 ->\n" + ret_string+=" am = am-1;\n" + ret_string+=" attacker_mem_"+str(index)+" ? "+fs+" -> attacker_mem_"+str(index)+" ! "+fs+";\n" + ret_string+=" :: am == 0 ->\n" + ret_string+=" attacker_mem_"+str(index)+" ? "+fs+" -> "+str(chan)+" ! "+fs+";\n" + ret_string+=" break;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n" + ret_string+=" b = len("+str(chan)+");\n" + ret_string+=" do\n" + ret_string+=" :: b != len("+str(chan)+") -> goto REPLAY;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: atomic {attacker_mem_"+str(index)+" ? "+fs+"; }\n" + ret_string+=" :: empty(attacker_mem_"+str(index)+") -> goto BREAK;\n" + ret_string+=" od\n" + ret_string+="BREAK:\n" + ret_string+="}\n" + + return ret_string + + +def gen_reorder(chan : str, chan_type : List[str], mem : int, index : int) -> str: + ret_string = "" + + ret_string+= "chan attacker_mem_"+str(index)+" = ["+str(mem)+"] of " + ("{ " + str(chan_type)[1:-1] + " }") .replace("'","") + ";\n" + ret_string+= "\n" + + ret_string+= "active proctype attacker_reorder_"+str(index)+"() priority 99 {\n" + + item_arr = [] + item_count = 0 + + attacker_mem = "attacker_mem_" + str(index) + + # formulate string of general message input variables + for item in chan_type: + item_arr.append("b_" + str(item_count)) + ret_string+= str(item) + " " + item_arr[item_count] + ";\n" + item_count+=1 + + fs = (str([item for item in item_arr])[1:-1]).replace("'","") + ret_string+="int i = "+str(mem)+";\n" + ret_string+="int b;\n" + ret_string+="INIT:\n" + ret_string+="do\n" + # ret_string+=" :: true -> {\n" + ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> {\n" + ret_string+=" b = len("+str(chan)+");\n" + ret_string+=" do\n" + ret_string+=" :: b != len("+str(chan)+") -> goto INIT;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: goto CONSUME;\n" + ret_string+="od\n" + ret_string+="CONSUME:\n" + ret_string+="do\n" + ret_string+=" :: "+str(chan)+" ? "+str(fs)+" -> atomic {\n" + ret_string+=" "+str(attacker_mem)+" ! "+str(fs)+";\n" + ret_string+=" i--;\n" + ret_string+=" if\n" + ret_string+=" :: i == 0 -> goto REPLAY;\n" + ret_string+=" :: i != 0 -> goto CONSUME;\n" + ret_string+=" fi\n" + ret_string+=" }\n" + ret_string+="od\n" + ret_string+="REPLAY:\n" + ret_string+=" do\n" + ret_string+=" :: atomic {\n" + ret_string+=" int am;\n" + ret_string+=" select(am : 0 .. len("+str(attacker_mem)+")-1);\n" + ret_string+=" do\n" + ret_string+=" :: am != 0 -> \n" + ret_string+=" am = am-1;\n" + ret_string+=" "+str(attacker_mem)+" ? "+str(fs)+" -> "+str(attacker_mem)+" ! "+str(fs)+";\n" + ret_string+=" :: am == 0 ->\n" + ret_string+=" "+str(attacker_mem)+" ? "+str(fs)+" -> "+str(chan)+" ! "+str(fs)+";\n" + ret_string+=" break;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: empty("+str(attacker_mem)+") -> goto BREAK;\n" + ret_string+=" od\n" + ret_string+="BREAK:\n" + ret_string+="}\n" + + return ret_string + +def gen_reorder_unbounded(chan : str, chan_type : List[str], index : int) -> str: + ret_string = "" + + ret_string+= "chan attacker_mem_"+str(index)+" = [99] of " + ("{ " + str(chan_type)[1:-1] + " }") .replace("'","") + ";\n" + ret_string+= "\n" + + ret_string+= "active proctype attacker_reorder_"+str(index)+"() priority 99 {\n" + + item_arr = [] + item_count = 0 + + attacker_mem = "attacker_mem_" + str(index) + + # formulate string of general message input variables + for item in chan_type: + item_arr.append("b_" + str(item_count)) + ret_string+= str(item) + " " + item_arr[item_count] + ";\n" + item_count+=1 + + fs = (str([item for item in item_arr])[1:-1]).replace("'","") + ret_string+="int b;\n" + ret_string+="INIT:\n" + ret_string+="do\n" + # ret_string+=" :: true -> {\n" + ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> {\n" + ret_string+=" b = len("+str(chan)+");\n" + ret_string+=" do\n" + ret_string+=" :: b != len("+str(chan)+") -> goto INIT;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: goto CONSUME;\n" + ret_string+="od\n" + ret_string+="CONSUME:\n" + ret_string+="do\n" + ret_string+=" :: "+str(chan)+" ? "+str(fs)+" -> atomic {\n" + ret_string+=" "+str(attacker_mem)+" ! "+str(fs)+";\n" + ret_string+=" do\n" + ret_string+=" :: goto REPLAY;\n" + ret_string+=" :: goto CONSUME;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+="od\n" + ret_string+="REPLAY:\n" + ret_string+=" do\n" + ret_string+=" :: atomic {\n" + ret_string+=" int am;\n" + ret_string+=" select(am : 0 .. len("+str(attacker_mem)+")-1);\n" + ret_string+=" do\n" + ret_string+=" :: am != 0 -> \n" + ret_string+=" am = am-1;\n" + ret_string+=" "+str(attacker_mem)+" ? "+str(fs)+" -> "+str(attacker_mem)+" ! "+str(fs)+";\n" + ret_string+=" :: am == 0 ->\n" + ret_string+=" "+str(attacker_mem)+" ? "+str(fs)+" -> "+str(chan)+" ! "+str(fs)+";\n" + ret_string+=" break;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: empty("+str(attacker_mem)+") -> goto BREAK;\n" + ret_string+=" od\n" + ret_string+="BREAK:\n" + ret_string+="}\n" + + return ret_string + +def gen_drop(chan : str, chan_type : List[str], mem : int, index : int) -> str: + ret_string = "" + + ret_string+= "active proctype attacker_drop_"+str(index)+"() {\n" + + # proctype variables + item_arr = [] + item_count = 0 + + + # formulate string of general message input variables + for item in chan_type: + item_arr.append("b_" + str(item_count)) + ret_string+= str(item) + " " + item_arr[item_count] + ";\n" + item_count+=1 + + fs = (str([item for item in item_arr])[1:-1]).replace("'","") + + ret_string+="byte i = "+str(mem)+";\n" + ret_string+="int b;\n" + ret_string+="MAIN:\n" + ret_string+=" do\n" + ret_string+=" :: "+str(chan)+" ? ["+fs+"] -> atomic {\n" + ret_string+=" if\n" + ret_string+=" :: i == 0 -> goto BREAK;\n" + ret_string+=" :: else ->\n" + ret_string+=" "+str(chan)+" ? "+fs+";\n" + ret_string+=" i = i - 1;\n" + ret_string+=" goto MAIN;\n" + ret_string+=" fi\n" + ret_string+=" }\n" + ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n" + ret_string+=" b = len("+str(chan)+");\n" + ret_string+=" do\n" + ret_string+=" :: b != len("+str(chan)+") -> goto MAIN;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: goto BREAK;\n" + ret_string+=" od\n" + ret_string+="BREAK:\n" + ret_string+="}\n" + + return ret_string + +def gen_drop_unbounded(chan : str, chan_type : List[str], index : int) -> str: + ret_string = "" + + ret_string+= "active proctype attacker_drop_"+str(index)+"() {\n" + + # proctype variables + item_arr = [] + item_count = 0 + + # formulate string of general message input variables + for item in chan_type: + item_arr.append("b_" + str(item_count)) + ret_string+= str(item) + " " + item_arr[item_count] + ";\n" + item_count+=1 + + fs = (str([item for item in item_arr])[1:-1]).replace("'","") + + ret_string+="int b;\n" + ret_string+="MAIN:\n" + ret_string+=" do\n" + ret_string+=" :: "+str(chan)+" ? ["+fs+"] -> atomic {\n" + ret_string+=" do \n" + ret_string+=" :: goto BREAK;\n" + ret_string+=" :: true ->\n" + ret_string+=" "+str(chan)+" ? "+fs+";\n" + ret_string+=" goto MAIN;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\n" + ret_string+=" b = len("+str(chan)+");\n" + ret_string+=" do\n" + ret_string+=" :: b != len("+str(chan)+") -> goto MAIN;\n" + ret_string+=" od\n" + ret_string+=" }\n" + ret_string+=" :: goto BREAK;\n" + ret_string+=" od\n" + ret_string+="BREAK:\n" + ret_string+="}\n" + + return ret_string diff --git a/src/utility.py b/src/utility.py new file mode 100644 index 0000000..c4c569b --- /dev/null +++ b/src/utility.py @@ -0,0 +1,168 @@ +import sys, re, subprocess, os, shutil +from typing import List + +def fileReadLines(fileName : str) -> str: + try: + txt = None + with open(fileName, 'r') as fr: + txt = fr.readlines() + return txt + except Exception: + return "" + +def fileRead(fileName : str) -> str: + try: + txt = None + with open(fileName, 'r') as fr: + txt = fr.read() + return txt + except Exception: + return "" + +def parse_channels(model : str) -> dict(): + channels = {} + define_mapping = {} + for line in model: + if line.startswith("#define"): + data = re.search(r"\#define\s*([A-Za-z\_\-]+)\s*([0-9])", line) + define_mapping[data.group(1)] = int(data.group(2)) + if line.startswith("chan"): + # parsing regular channels + data = re.search(r"chan\s*([a-zA-Z\_\-]+).*\{(.+)\}", line) + # note, we don't have to think very hard about parsing Promela types. + # this is because mtype:whatever, mtype, and generic types are interchangable in Promela grammar + name, ctype = data.group(1), data.group(2).replace(" ","").split(",") + channels[name] = list(tuple(ctype)) + + # data_multichan = re.search(r"chan\s*([A-Za-z\_\-0-9]+)\[([A-Za-z0-9\_\-]+)\].*\{(.+)\}", line) + # m_name, m_cvalue, m_ctype = data.group(1), data.group(2), data.group(3).replace(" ","").split(",") + + # try: + # m_cvalue = int(c_value) + # except ValueError: + # if type(m_cvalue) == str: + # assert m_cvalue in define_mapping, "{c_value} isn't defined, yet your Promela file still parsed. Did you recursively define {c_value}?" + # m_cvalue = define_mapping[m_cvalue] + + # channels[m_name] = (m_cvalue, m_ctype) + + else : continue + # print(channels) + return channels + +def parse_mchannels(model : str) -> (dict(), dict()): + channels = {} + channel_lens = {} + define_mapping = {} + for line in model: + if line.startswith("#define"): + data = re.search(r"\#define\s*([A-Za-z\_\-]+)\s*([0-9])", line) + define_mapping[data.group(1)] = int(data.group(2)) + # print(define_mapping) + if line.startswith("chan"): + # parsing multichannels + data_multichan = re.search(r"chan\s*([A-Za-z\_\-0-9]+)\[([A-Za-z0-9\_\-]+)\].*\{(.+)\}", line) + if data_multichan: + m_name, m_cvalue, m_ctype = data_multichan.group(1), data_multichan.group(2), data_multichan.group(3).replace(" ","").split(",") + else : continue + + try: + m_cvalue = int(m_cvalue) + except ValueError: + if type(m_cvalue) == str: + assert m_cvalue in define_mapping, "{m_cvalue} isn't defined, yet your Promela file still parsed. Did you recursively define {c_value}?" + m_cvalue = define_mapping[m_cvalue] + + channels[m_name] = m_ctype + channel_lens[m_name] = m_cvalue + + + else : continue + # print(channels) + + return channels, channel_lens + +def ensure_compile(model_path : str) -> None: + cmd = ['spin', '-a', model_path] + proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + stdout, stderr = proc.communicate() + filename = os.path.basename(model_path) + userdir = os.getcwd() + + # Convert bytes to string + stdout = stdout.decode() + stderr = stderr.decode() + assert "error" not in stdout, "there seems to be a syntax error in the model!" + # assert "syntax error" not in stdout, "there seems to be a syntax error in the model" + # assert "processes created" in stdout, "the spin model creates no processes ... check to see if it compiles" + +def eval_model(model_path : str) -> None: + cmd = ['spin', '-run', '-a', '-DNOREDUCE', model_path] + # Set text=True to get string output + proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True) + + out = "" + while True: + output = proc.stdout.readline() + if output == '' and proc.poll() is not None: + break + if output: + out+=output + print(output, end='') + + # No need to decode since output is already a string + # stdout, stderr = proc.communicate() + + # filename = os.path.basename(model_path) + # userdir = os.getcwd() + + # print(stderr) + + if "pan: wrote" in out: # we know we wrote a trail + print("attack trace found!!!! printing!\n") + cd = os.getcwd() + if "/" in model_path: + od = cd + model_path[model_path.rindex("/"):] + ".trail" + shutil.copy(od, model_path + ".trail") + shutil.copy(cd + "/pan", model_path[:model_path.rindex("/"):] + "/pan") + else: + od = cd + model_path + ".trail" + # shutil.copy(od, model_path + ".trail") + # shutil.copy(cd + "/pan", model_path[:model_path.rindex("/"):] + "/pan") + + cmd = ['spin', '-t0', '-s', '-r', model_path] + proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + stdout, stderr = proc.communicate() + filename = os.path.basename(model_path) + userdir = os.getcwd() + + # Convert bytes to string + stdout = stdout.decode() + stderr = stderr.decode() + + print(stdout) + else: + print() + print("Korg's exhaustive search is complete, no attacks found :)") + +def cleanup_spin_files() -> None: + """Remove files generated by Spin""" + files_to_remove = [ + 'pan', 'pan.*', '*.trail', '_spin_nvr.tmp', + '*.tcl', 'pan.b', 'pan.c', 'pan.h', 'pan.m', 'pan.t' + ] + for pattern in files_to_remove: + if '*' in pattern: + import glob + for f in glob.glob(pattern): + try: + os.remove(f) + print(f"Removed: {f}") + except OSError: + pass + else: + try: + os.remove(pattern) + print(f"Removed: {pattern}") + except OSError: + pass diff --git a/test_harness.py b/test_harness.py new file mode 100644 index 0000000..2153d29 --- /dev/null +++ b/test_harness.py @@ -0,0 +1,65 @@ +import yaml, sys +import sys, re, subprocess, os, shutil +from typing import List + +passed = 0 +failed = 0 + +def show_help() -> None: + msg=""" Usage: + python3 test_harness.py tests/tests.yaml + """ + print(msg) + +def run_spin_test(name, data): + global passed + global failed + data = {k: v for d in data for k, v in d.items()} + cmd = data['command'] + intended = data['intended'] + explanation = data['intended'] + + proc = subprocess.Popen(cmd.split(" "), stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True) + + out = "" + while True: + output = proc.stdout.readline() + if output == '' and proc.poll() is not None: + break + if output: + out += output + + res = None + if "assertion violated" in out: + res = "property violation" + elif "acceptance cycle" in out: + res = "acceptance cycle" + else : res = "no violation" + + if res == intended: + print("passed: " + name) + passed+=1 + else: + print("FAILED: " + name + " - got '" + res + "', expected '" + intended + "'") + failed+=1 + + +def main() -> None: + args = sys.argv[1:] + + if len(args) == 0 or args[0] in ["help", "--help", "-h", "-help"]: + show_help() + sys.exit() + + test_file = args[0] + + file = open(test_file, 'r') + data = yaml.safe_load(file) + for i in data: + run_spin_test(i, data[i]) + + print("") + print("SUMMARY:") + print("passed: " + str(passed) + "; failed: " + str(failed)) + +main() diff --git a/tests/drop/t1-drop.pml b/tests/drop/t1-drop.pml new file mode 100644 index 0000000..d5f3281 --- /dev/null +++ b/tests/drop/t1-drop.pml @@ -0,0 +1,20 @@ +// INTENDED BEHAVIOR: acceptance cycle +chan c = [8] of { byte }; +byte q=1; + +init { +c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC; + od +PROC: + q=0; +} + +ltl proc { + eventually (q == 0); +} diff --git a/tests/drop/t2-drop.pml b/tests/drop/t2-drop.pml new file mode 100644 index 0000000..d7952ed --- /dev/null +++ b/tests/drop/t2-drop.pml @@ -0,0 +1,22 @@ +// INTENDED BEHAVIOR: no violation +// explanation: attacker can only drop one message, but two are on the channel +chan c = [8] of { byte }; +byte q=1; + +init { +c!5; +c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC; + od +PROC: + q=0; +} + +ltl proc { + eventually (q == 0); +} diff --git a/tests/drop/t3-drop.pml b/tests/drop/t3-drop.pml new file mode 100644 index 0000000..44b54a7 --- /dev/null +++ b/tests/drop/t3-drop.pml @@ -0,0 +1,22 @@ +// INTENDED BEHAVIOR: violation +// explanation: attacker should be able to drop both messages +chan c = [8] of { byte }; +byte q=1; + +init { +c!5; +c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC; + od +PROC: + q=0; +} + +ltl proc { + eventually (q == 0); +} diff --git a/tests/drop/t4-drop.pml b/tests/drop/t4-drop.pml new file mode 100644 index 0000000..369e2b3 --- /dev/null +++ b/tests/drop/t4-drop.pml @@ -0,0 +1,24 @@ +// INTENDED BEHAVIOR: violation +// explanation: drop attacker should be able to find the attack in the middle of the chan +chan c = [8] of { byte }; +byte q=1; + +init { +c!3; +c!5; +c!6; + +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC; + od +PROC: + q=0; +} + +ltl proc { + eventually (q == 0); +} diff --git a/tests/drop/t5-drop-multi.pml b/tests/drop/t5-drop-multi.pml new file mode 100644 index 0000000..35006e4 --- /dev/null +++ b/tests/drop/t5-drop-multi.pml @@ -0,0 +1,24 @@ +// INTENDED BEHAVIOR: acceptance cycle +chan c = [8] of { byte }; +byte q=1; + +init { +c!5; +c!5; +c!5; +c!5; +c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC; + od +PROC: + q=0; +} + +ltl proc { + eventually (q == 0); +} diff --git a/tests/drop/t6-drop-overwhelm.pml b/tests/drop/t6-drop-overwhelm.pml new file mode 100644 index 0000000..35006e4 --- /dev/null +++ b/tests/drop/t6-drop-overwhelm.pml @@ -0,0 +1,24 @@ +// INTENDED BEHAVIOR: acceptance cycle +chan c = [8] of { byte }; +byte q=1; + +init { +c!5; +c!5; +c!5; +c!5; +c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC; + od +PROC: + q=0; +} + +ltl proc { + eventually (q == 0); +} diff --git a/tests/reorder/t1-reorder.pml b/tests/reorder/t1-reorder.pml new file mode 100644 index 0000000..bc7f889 --- /dev/null +++ b/tests/reorder/t1-reorder.pml @@ -0,0 +1,30 @@ +// intended behavior: no violation +// explanation: the rearrange attacker gadget shouldn't be able to violate the claim, as +// it doesn't have enough mem +chan c = [8] of { byte }; +byte q=0; + +init { +c!3; +c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> + q = q+1; + goto B1; + od +B1: + do + :: c ? 3 -> + q = q + 1; + goto END; + od +END: +} + +ltl proc { + always !(q==2); +} diff --git a/tests/reorder/t2-reorder.pml b/tests/reorder/t2-reorder.pml new file mode 100644 index 0000000..7e7d812 --- /dev/null +++ b/tests/reorder/t2-reorder.pml @@ -0,0 +1,36 @@ +// intended behavior: violation +// explanation: rearrange attacker has enough mem to do the rearrange attack +chan c = [8] of { byte }; +byte q=0; + +init { +c!3; +c!5; +c!7; +} + +active proctype consume() { +MAIN: + do + :: c ? 7 -> + q = q+1; + goto B1; + od +B1: + do + :: c ? 5 -> + q = q + 1; + goto B2; + od +B2: + do + :: c ? 3 -> + q = q + 1; + goto END; + od +END: +} + +ltl proc { + always !(q==3); +} diff --git a/tests/reorder/t3-reorder.pml b/tests/reorder/t3-reorder.pml new file mode 100644 index 0000000..86e8021 --- /dev/null +++ b/tests/reorder/t3-reorder.pml @@ -0,0 +1,36 @@ +// intended behavior: no violation +// explanation: rearrange attacker does not have enough mem +chan c = [8] of { byte }; +byte q=0; + +init { +c!3; +c!5; +c!7; +} + +active proctype consume() { +MAIN: + do + :: c ? 7 -> + q = q+1; + goto B1; + od +B1: + do + :: c ? 5 -> + q = q + 1; + goto B2; + od +B2: + do + :: c ? 3 -> + q = q + 1; + goto END; + od +END: +} + +ltl proc { + always !(q==3); +} diff --git a/tests/reorder/t4-reorder.pml b/tests/reorder/t4-reorder.pml new file mode 100644 index 0000000..5324b72 --- /dev/null +++ b/tests/reorder/t4-reorder.pml @@ -0,0 +1,34 @@ +// intended behavior: violation +// explanation: rearrange attacker does not have enough mem +chan c = [1] of { byte }; +byte q=0; + +init { +c!3; +c!5; +c!7; +} + +active proctype consume() { +MAIN: + do + :: c ? 3 -> + goto B1; + od +B1: + do + :: c ? 7 -> + goto B2; + od +B2: + do + :: c ? 5 -> + goto END; + od +END: +q = 1; +} + +ltl proc { + always !(q == 1); +} diff --git a/tests/replay/3-jump.pml b/tests/replay/3-jump.pml new file mode 100644 index 0000000..e17378a --- /dev/null +++ b/tests/replay/3-jump.pml @@ -0,0 +1,29 @@ +// INTENDED BEHAVIOR: no violation +// explanation: can only replay once +chan c = [8] of { byte }; +byte q=1; + +init { +c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC1; + od +PROC1: + do + :: c ? 5 -> goto PROC2; + od +PROC2: + do + :: c ? 5 -> goto PROC3; + od +PROC3: + q=0; +} + +ltl proc { + always !(q == 0); +} diff --git a/tests/replay/replay-out-of-order.pml b/tests/replay/replay-out-of-order.pml new file mode 100644 index 0000000..eb00527 --- /dev/null +++ b/tests/replay/replay-out-of-order.pml @@ -0,0 +1,34 @@ +// INTENDED BEHAVIOR: violation +// explanation: replay, but in a different order than received +chan c = [8] of { byte }; +byte q=1; + +init { +c!5; +c!3; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC1; + od +PROC1: + do + :: c ? 3 -> goto PROC2; + od +PROC2: + do + :: c ? 3 -> goto PROC3; + od +PROC3: + do + :: c ? 5 -> goto PROC4; + od +PROC4: + q=0; +} + +ltl proc { + always !(q == 0); +} diff --git a/tests/replay/t1-replay.pml b/tests/replay/t1-replay.pml new file mode 100644 index 0000000..ed28804 --- /dev/null +++ b/tests/replay/t1-replay.pml @@ -0,0 +1,24 @@ +// INTENDED BEHAVIOR: violation +chan c = [8] of { byte }; +byte q=1; + +init { +c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC1; + od +PROC1: + do + :: c ? 5 -> goto PROC2; + od +PROC2: + q=0; +} + +ltl proc { + always !(q == 0); +} diff --git a/tests/replay/t2-replay.pml b/tests/replay/t2-replay.pml new file mode 100644 index 0000000..ad87d40 --- /dev/null +++ b/tests/replay/t2-replay.pml @@ -0,0 +1,19 @@ +chan c = [8] of { byte }; +byte q=1; + +init { +c!5; +} + +active proctype consume() { +MAIN: + do + :: c ? 5 -> goto PROC; + od +PROC: + q=0; +} + +ltl proc { + eventually (q == 0); +} diff --git a/tests/tests.yaml b/tests/tests.yaml new file mode 100644 index 0000000..8d926a7 --- /dev/null +++ b/tests/tests.yaml @@ -0,0 +1,76 @@ +t1-reorder: + - command: python src/main.py --model=tests/reorder/t1-reorder.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: the reorder attacker gadget shouldn't be able to violate the claim, as it doesn't have enough mem + +t1-reorder-more-mem: + - command: python src/main.py --model=tests/reorder/t1-reorder.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=2 + - intended: property violation + - explanation: the reorder attacker now has enough mem + +t2-reorder: + - command: python src/main.py --model=tests/reorder/t2-reorder.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=3 + - intended: property violation + - explanation: rearrange attacker has enough mem to do the reorder attack + +t3-reorder: + - command: python src/main.py --model=tests/reorder/t3-reorder.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: rearrange attacker does not have enough mem + +t4-reorder: + - command: python src/main.py --model=tests/reorder/t4-reorder.pml --attacker=reorder --chan=c --output=temp.pml --eval --cleanup --mem=2 + - intended: no violation + - explanation: rearrange attacker does not have enough mem + +t1-drop: + - command: python3 src/main.py --model=tests/drop/t1-drop.pml --attacker=drop --chan=c --output=temp.pml --mem=1 --eval --cleanup + - intended: acceptance cycle + - explanation: drop attacker is able to remove the single message on the channel, preventing the eventually LTL property from ever satisfying + +t2-drop: + - command: python3 src/main.py --model=tests/drop/t2-drop.pml --attacker=drop --chan=c --output=temp.pml --mem=1 --eval --cleanup + - intended: no violation + - explanation: drop attacker is not able to remove both the messages on the channel, so the LTL property remains satisfying + +t3-drop: + - command: python3 src/main.py --model=tests/drop/t3-drop.pml --attacker=drop --chan=c --output=temp.pml --mem=2 --eval --cleanup + - intended: acceptance cycle + - explanation: attacker should drop both messages + +t4-drop: + - command: python3 src/main.py --model=tests/drop/t4-drop.pml --attacker=drop --chan=c --output=temp.pml --mem=1 --eval --cleanup + - intended: acceptance cycle + - explanation: drop attacker should be able to find the attack in the middle of the chan + +t5-drop-multi: + - command: python3 src/main.py --model=tests/drop/t5-drop-multi.pml --attacker=drop --chan=c --output=temp.pml --mem=5 --eval --cleanup + - intended: acceptance cycle + - explanation: attacker can drop all five messages + +t6-drop-overwhelm: + - command: python3 src/main.py --model=tests/drop/t6-drop-overwhelm.pml --attacker=drop --chan=c --output=temp.pml --mem=4 --eval --cleanup + - intended: no violation + - explanation: attacker can't drop all five messages + +t1-replay: + - command: python src/main.py --model=tests/replay/t1-replay.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=1 + - intended: property violation + - explanation: since the attacker is able to replay "5" on c, they can progress the consume proctype from PROC1, then PROC2 + +t2-replay: + - command: python src/main.py --model=tests/replay/t2-replay.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: the attacker must eventually replay the packet onto the channel + +3-jump: + - command: python src/main.py --model=tests/replay/3-jump.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: can only replay the packet once + +replay-out-of-order: + - command: python src/main.py --model=tests/replay/replay-out-of-order.pml --attacker=replay --chan=c --output=temp.pml --eval --cleanup --mem=2 + - intended: property violation + - explanation: replay, but in a different order than received + +