From f5820eb211946cc01e06a42c48646e1a7df54a8d Mon Sep 17 00:00:00 2001 From: Jake Ginesin Date: Mon, 10 Nov 2025 13:59:52 -0500 Subject: [PATCH] readme update --- README.md | 28 +++++++++++++++++- .../model_generate.cpython-313.pyc | Bin 20378 -> 17683 bytes src/model_generate.py | 4 +-- tests/tests.yaml | 10 +++++++ 4 files changed, 39 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 12144e0..35b08b9 100644 --- a/README.md +++ b/README.md @@ -12,13 +12,39 @@ - [x] make the impl more robust; do more SWE - [x] add no self-deadlock experiments - I envision this would be: providing an eventually-style LTL query, sending messages onto an open channel, and asserting that the gadget doesn't somehow deadlock with itself +- [ ] support queries over multiple properties - [ ] add raft, TCP, SCTP, ABP experiments from old Korg impl to the test suite - [ ] add labels on trace logging to gadgets - [ ] modify the paper? spin workshop? # Notes - Sound and complete attack discovery for replay, dropping, and reordering attacks on channels - - possible because of the finite-state modeling spin does + - possible because of the finite-state modeling spin does. Indeed, we can model no-limit attackers within the finite-state model, giving guarantees of decidability and complexity. - 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. - One explicit limitation of the replay attacker is not being able to transition back to listening for packets after replaying - Maybe change the title to: Korg: Automated analysis of channel faults +- The inclusion of the pass on chan functionality is required to ensure liveness properties are not trivially violated by an attacker gadget that loops with itself. Thus the pass on chan functionality is the best possible "wait" we could think up. We also include no deadlock tests. + +# Gadget Structures + +Drop: +- drop msg off chan +- pass on chan + +Replay: +:CONSUME: +- consume msg; may go to CONSUME or REPLAY +- pass on chan +:REPLAY: +- replay msg +- pass on chan +- pass on chan, then go to REPLAY + +Reorder: +:INIT: +- pass msg on chan +- go to CONSUME +:CONSUME: +- consume n messages on chan, then go to REPLAY +:REPLAY: +- replay msg diff --git a/src/__pycache__/model_generate.cpython-313.pyc b/src/__pycache__/model_generate.cpython-313.pyc index fd345dfd41f1e137d95ac5e868c80aabdf84814f..58b0958ca01941c415c8efb67cd4ab8556d595c0 100644 GIT binary patch delta 2362 zcmbW2O>7%Q6vuaxU4N|YbrRc&9TR6=w@sW+JFOt8<1}vKHlI$3>q2Rpuf`2&61$xw zM0F`?;ef=2L{CDf2+9Et<XylEV96^Z@x55clNF-PGVTCSy@dhs~?raULxyFmBJ~JnpelF z^k!~aAV6Fu3%8Xi;#c4h>COIZ9nxoS=@kN>S4_HcdX-%#r{$aujq`F&e_UJ6&_9z@QG zEM~S}7D?9cIwnC^#6hmZ8>AjS^(3rfLX69e7C}g%WrAyxtJK`ca@2gyLQ0BT;QbOG zQQ*gtwrVTBd-AY^BiJu)+#H+G#U;33)CHc_+G;UgvJtg(!z#;L5b)N+N~SqoBVKHQivUHN^S@^6kM=% zSHa%~F_fhdee0?12CsvsCh?JQvB?grWj3QP|Mz)S{zpeK{lS&BN`AGn>Hf?h&nj3qjR|i%?`v~L?j23-(|RAdu%vpP2_kyEs_OsHXXHkqo`M5%%A19du{aUGb0 zJ`#dJuz_UYolF~W$vYKRPTRt!@AH{*k5JiaNhzf)gQHdBqj3TNK9t5wdF|>G9@hTd} z#|ea{Bw8mBlL$8=gh(PzB76c1#sw@aYpsAoat1s*DwcT}^RnBbKTe-QJdNNRF^v{# zPER3t6>kbYgFarU|E95Vi^h3**VXl*ymS_!smiQ>7B-B8-BOyp7|T8vuF*+uR0V!% zXvfAV@wN$PL>p^Wvis=9gLSu+Q#KX>`0V`vYrccu)HtaHC$=O&b zToCS*+Ol6qmkAuJ3d6!+EPL-jXOY!~neh%-oG6Z0^2YyzU4p+_?PwDZWcs}Dc3+hm z-M6 z(r1{@Z+Q6L@vYn3H3J*2oqu*96L7WPX*$bXH!B+^}WCwkL`Pg3w^Bx$AIYMLt9a` zNh@`Q-m0zolS<7;_=rSgsg2YsiQ0TbT~e%mB&DtLQB|tcRwYWl+@H=J$1ir4w)yCj zeBOO`=FZH$bLWoXRr0}UV!mxM83p$Ic1Aq>`?@)EK5@@g%t8?{8jN<~h?a_T2MY`$ z7qdYoiXofJCRCfaXhyYY=CU+GJQA!Wn=`z6Sgfy%&XZ3wAm7jkpJ~jb1m+BiQd-64 zt1<~fMBA$km8nuWwo0zF)(Y6EwLo#H6{a;ts4L9{U0$J4H7SEOT>+_qOSuZEg}FS( z+gdlAD>bUBKl40b*4o87)g&?ES)N5pK2?>1$A33qLD${^>k))#+?%at=&R4h$U))BdsWSpT$+8%$>foP#tx za5P|~>(Hth(ZT>1MI}Jj<7X?P4bhGWA~qm4A~rKjWHIo05VVVZMZeG9ud`{Glza?K z!0+2X>fnXuO33ui8heRF=wQ=D^l;H@1Ggm`erfg*3FN8(bhWtPip8Zf^lCyf{Mu58 zX$>x`46m&>n{w5Z(DZ6xr?pr#@bt+?!g7OBuAtPL&}OCf4%vCKFuRZgcK9lY)llsJCaa|PsA7vc)4+>e;mqgqv}(kisb@usY~3gv(C z#FuVwO0}O-i9qxB%>`F}|9`Amv+fa(yK#dHf|D`FdBJED_eB9j3Zg%9n5S-V}_$5iiO zn^g<9vX$sH`!s=yy8pkFNPF*<5|6mm6P+r0N$==kONpBkD;#t-J4eG2cOpdHU~yII zL#&;8Am}P3ei(6i9kc>9ywdcdREt=NSPfsgR_W_d^uk{*Wu}3NiQ3A%=j9}Tjl8Dd zro=_QiQ%zhlPBDXV#0SLy`p%GDdEOK_^_BSWv7<2#144*7T_hEa1Y6A(UO=b?c;Pf zOzAP!;f4^sRBf`F^DKY6e2K)bO^zds~e?ZL>Q3>Axei3 zBM1k=k9Z1k7*Q(BFk*hwKExgbPu}|jjSWW-M-e>YqbOm(=@{a^Xh%@TtM$VIoRtjl zUe@bj2|bSH_pb{hl64Cyt$l&-?WH>xbDKk_EOZM{`Om?_t-xA%w=Aur@!2`%o zIsR2~V7(Pjg#d5ya`@W6pyz)2;l(De7PAq~H7PT3 z*@O2UFALk-Hh11V{qdZ8)uO$7W7}4yPY=YrhHhem&PKwz~C!xEwmQ2CP)(%S|3aCAfz;t1eu=hNTU(X=Y9i=Bw$2R)@;>0vd zE0VsYY~gdP;Us!_i$F)98X6oY!57Sew}g~aj9TsJm8JT)3_p)WHXn_HL&GA?TfAvXor zb;0$W;QC3hEo)l|$$P(aS-|(%wF{bge?qJp+zzIHNtqR`54jxQZJ9 diff --git a/src/model_generate.py b/src/model_generate.py index 0db573e..4729af0 100644 --- a/src/model_generate.py +++ b/src/model_generate.py @@ -443,7 +443,7 @@ def gen_drop(chan : str, chan_type : List[str], mem : int, index : int) -> str: ret_string+=" goto MAIN;\n" ret_string+=" fi\n" ret_string+=" }\n" - ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\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 MAIN;\n" @@ -484,7 +484,7 @@ def gen_drop_unbounded(chan : str, chan_type : List[str], index : int) -> str: ret_string+=" goto MAIN;\n" ret_string+=" od\n" ret_string+=" }\n" - ret_string+=" :: "+str(chan)+" ? ["+str(fs)+"] -> atomic {\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 MAIN;\n" diff --git a/tests/tests.yaml b/tests/tests.yaml index f9f1255..190f9ee 100644 --- a/tests/tests.yaml +++ b/tests/tests.yaml @@ -1,3 +1,13 @@ +unidirectional-drop-abp: + - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol + +bidirectional-drop-abp: + - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1 + - intended: no violation + - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol + drop-nodeadlock: - command: python src/main.py --model=tests/no-deadlocks/t1-deadlock.pml --attacker=drop --chan=c --output=temp.pml --eval --cleanup --mem=2 - intended: no violation