From 558170c0621a93895161e1cc8160e00087549c6a Mon Sep 17 00:00:00 2001 From: Yorick Barbanneauwq Date: Wed, 15 Mar 2023 23:01:53 +0100 Subject: [PATCH] Add second part of verification --- .../2_verification/index.md | 83 +++++++++++++++++- .../files/q1/magic | Bin 16680 -> 0 bytes 2 files changed, 79 insertions(+), 4 deletions(-) delete mode 100755 content/secu_logicielle/td5-stackoverflow_shellcode/files/q1/magic diff --git a/content/conception_formelle/2_verification/index.md b/content/conception_formelle/2_verification/index.md index 93f43ae..a5654d6 100644 --- a/content/conception_formelle/2_verification/index.md +++ b/content/conception_formelle/2_verification/index.md @@ -224,7 +224,82 @@ transitions: \\(T\\) comme transitions * \\(\text{coreach}(S,T)\\) représente tous les états avec comme destnation \\(S\\) et utilisants \\(T\\) comme transitions. - * \\(\text{loop}(T_1,T_2)\\) représente les *Strongly Connected Components* - (SCC). C'est une formule de transition tel que \\(T_3 \subseteq T_2\\) et - \\(T_3 \cap T_1 \neq \emptyset\\) - + * \\(\text{loop}(T_1,T_2)\\) calcule des transition, elle représente les + *Strongly Connected Components* (SCC). C'est une formule de transition tel + que \\(T_3 \subseteq T_2\\) et \\(T_3 \cap T_1 \neq \emptyset\\). Ces *SCC* + déterminent toutes situations permettant de revenir à la situation initiale. + +## ARC + +*ARC* est le *model checker* d'Altarica, c'est un interpréteur de commande. + +### Les propriétés + +En plus des propriétés heritées de la logique de *Dicky*, il existe dans ARC les +propriété calculées suivantes pour chaque nœud: + + * `epsilon` : + * `self` : transitions dont la source est la destination sont égaux + * `self-epsilon`L définis par \\(epsilon \cap self \\) + * `not_deterministic`: ensemble de transition non déterministe definies plus + formellement par + \\(\\{(s,e,t_1) \in E | \exists t_2 /in V, (s,e,t_2) \in E\\}\\) + +#### Exemple + +``` +with Switch, CircuitV1, Scheduler do + deadlock := any_s - src(any_t - self_epsilon); + notSCC := any_t - loop(any_t, any_t); +done +with CircuitV1, CircuitV2, CircuitV1_OK do + bug := [L.on & ~L.ok]; + notControl := (label G.failure | label L.reaction | epsilon) - self_epsilon; + + // IR means infinite reactions + IR := loop(notControl, notControl); +done +``` +### Les opérateurs + +En plus des oérateurs disponibles dnas la logique de Dicky, ARC implémente les +opérateurs suivants: + + * \\(trace(S_1, T, S_2)\\) : ensemble de transitions représentant le chemin le + plus long de \\(S_1\\) vers \\(S_2\\) en utilisant les transitions\\(T\\). + * \\(project(S,T, 'newNodeName', boolean, aNode)\\) : construit une nouveau + nœud AltaRica avec toutes les transitions \\(T\\) prenant leurs origines dans + \\(S\\) en restectant les déclarations de \\(aNode\\) (cette déclaration est + facultative). + +`trace` nous sera utile pour trouver des contre-exemple et `project` pour +calculer des contrôleurs pour notre système. + +### Methodologie + +nous allons utiliser cet outils ocmme un **déboggeur de modèle**, en respectant +les étapes suivantes: + + 1. identifier les composants de base + 2. choisir entre le design *fonctionnel* ou *architectural* en fonction de + l'objectif et de ce que l'on sait faire. + 3. choisir entreun système **ouvert** ou **fermé** (restreindre le système a + des cas d'utilisation) + 4. construire l'arborescence du bas vers le haut + +### Validation d'un premier modèle + + 1. validation de la topologie du graphe (*SCC*, *deadlock*) + 2. propriété dépendantes de l'application (pas de réaction infinie) + 3. toues les évèmements sont utiles + 4. visualisation de petits composants + 5. simutation + +les étapes 1 et deux sont à répéter jusqu'à obtention d'un modèle valide. + +### Vérification du modèle + +Les spécification son écrites comme une liste de propiété logique et utilise la +logique de *Dicky* enrichie des éléments vu dans cette partie. Pour chacune des +propriétés ne satifaisant pas le modèle, **un contre exemple le plus petit +possible doit être calculé**. diff --git a/content/secu_logicielle/td5-stackoverflow_shellcode/files/q1/magic b/content/secu_logicielle/td5-stackoverflow_shellcode/files/q1/magic deleted file mode 100755 index c3255cfd475fbdb69b49c093d4a35dc2b19ebf50..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 16680 zcmeHOe~cVe9e*>sd%NxS?zVS8uN1s#X|W);dv`6hrIgO~?%FxIQY-~AMu)xKx!nnS zyT|S<9B50S6+DYcON=(A(ds{Hf{8}|AkpAqg;GNl;*ZpS^du0^pjaXr1Y!Mt-}`>| z=Egf9XyQNfO=iA7-uLr;Z@%x%?3+(Ph!(I!;V@+hawRc8ud4#)3G#~oM_d;QlA8Y^8i|jhLXJuDCj5|0oLLrU*Ah{>+ESpE=fnbjwR#{{7TQ@|+H=#bLO(2Ku&s>OgtkD}Ne356=z9?yn0CZJ_T9_hxbm%E zxKlS?{fEci{K<*T&zE+LV6UBbs!qYJc~14f-oa9(>>S9Bl^kK)g^5bpu6fz2XWK%$F5w71xjXG# z@lJa@>y`is{gor+MAj_}&?m6FwxE<#(w@-6lw=7qRS5vyDar@qK?8nSTCL*7OV3kryxAd|xc8!vFL`45W<=se!XwTIy-z4 zW53*C9UDGrogI4WG^*B-;ggzmwY3tanujj1~T_llSZ0>t+HyYYa-k6Z5F>rU3Q_- zC;`77IJ`EC67buBuY0x8_#$xpW{ITTw_j*eDQ(S)c;YyG_`>gH_^tlJUmJ}p(P1c_ zLR&8!DqGZ1DV%s`ldFau!*!VH8N2s037Ak09R0nC5_A77C!&^l*co9IgG z{8~j^>xi^MF?f+Pr38x}B^{+Wt4Zhe%WFvISFuY;pQZK6`2L2(<$r&>Q9*qsVj@#( zv4KxUO;qKYXXLX~z8n>xM->xE;$6fqCeDo4M$XYXNr_tg{~P1=+tACy`P{yCuOvE#s6qA|DZLEsqvxuD;v9Iir^kbgJC(v|YDW+rGACTXLjRhmjNAEFuXsCAY1OD^qNxwxO*v8R=fr zy;AFlr(j&RP&7zbJgx0q4N;PSNPckjNGJN3U7uO4K?Mm-!+Msj6(gM)ygv$X#Ndv* z8n~uuZ??4}!x0Gw2;FjU>RPwnuFEcvr`S5NOy~5hdNHHkSFW{Db&j~w@`NS23nd*u9&R~xgZr*C_z~gR_ zDOM(&j5Arx)|^bflB-WRWv`a0xt>$Y7d z6x^KaluAy<%U=ss!%FkY-A;A9RJq5l6`>$k$vc^Gw*VvBT|8x%0{0@YvkBV0t zi@7Xj$LEbEE*8Q2wnGM3DR{pG$J-$NR|$Upv3)xT3d0t~am*VFO;Y=+w0DVwX)Y-B zKud`(f$MJk^l4B!V9@jL1eZO4c2<1+6v!AS82{T~H++69J`Tc4xOY;4dY?i&{_AL% z(iQ)^MEVsRDX|*NCaO*PEl3@Do0z2MoqRxm?HgzpZO#2o^1n;4y$T1$31078>WD%>QZ}}V-H*Q?)?LMhiz+U zzp(d=?%OpmYVX^<`_^zCwZ$88r*KI>(LJ?@rWh_Y~NMKj1| zC_+EA$pVyxdo}EQtzs9m`52* ze2mp<6jMGYY#a83*uyssz4HzbXe*4#bnV^=FFOX@t14b(2_6PcbyB3u70*c*%Jnqd z@RLr}yVqwLtGlqn$IX*zVAn{Gmn{hC4$qFFNayb@Llug9RaFAdf|^??FHmeKgUibz zfTYQiC(^Q+Y0sGgS>`ugt;lSrouWNn%}zLWF%MYQ6vEC{t669$B3OpN*$FoXwN@Y& zoYJxa6%2AH(z(h6KIfpZ&RD$wxNN!LfL*C>dA!1Mc5JNb+|3&7aB^6N?6HVu=$LAA zX#O|C8UVwPhp!Eax+10&c>f>I7pYkKvW)x+IO1?Hp7*u!em4`!{KWG&wrv5ykLUeu zyzdRaOZbVOCu|!5!H+*h?LS2mPlFwa2l2Sy>K`yCbLQ&yP3gxo;5O@Pk1nbCZ8FfHw(mlH)+2 z!x+zDzZ1ao@Ac7@%A=JXi3i*NeZqIJpJ6J=P%P-rI`bcb8#a;qkLNE@!e67pG|!A< z!#NQA_+F~N*H9jhup@EqKQ{jo1bnZc+ePquEbj{q`m@gb_keBp;rTsxwg-$r?5DJO zo$W6}0gfH6pXYVF&v%yk563?eKbMz*jmM5csPpk_6;E?RsW70z SyTao5Cvai_G#&s1RPk?I8ZD*(