question 5

sujet.md

@@ -12,7 +12,8 @@
 
 ## Answers
 
-1. Software bug :
+### 1. Software bug :
+
 I found the article of Chromium that still exists today. It seems that fixed it in some of their application but still visible in Google Maps, Youtube,....
 Here is the link to the issue:
 https://issues.chromium.org/issues/391788835
@@ -41,7 +42,8 @@ Liability concerns
 Would Testing the Right Scenario Have Caught the Bug?
 Yes by security testing specially in visual spoofing but this bug is quite rare and it is normally being exploited in early 2006 era so it is understandable that it is hard to detect.
 
-2. Apache Bug :
+### 2. Apache Bug :
+
 COLLECTIONS-799: "UnmodifiableNavigableSet can be modified by pollFirst() and pollLast()"
 https://issues.apache.org/jira/projects/COLLECTIONS/issues/COLLECTIONS-799?filter=doneissues
 Il s'agit d'un bug local qui permet de modifier `UnmodifiableNavigableSet`, un Set censé être immutable, via les fonctions `pollFirst()` et `pollLast()`, ces deux fonctions sont héritées de la classe `AbstractNavigableSetDecorator` qui elle est mutable.
@@ -50,7 +52,8 @@ Il a ensuite commit la correction qui consiste simplement à override `pollFirst
 
 
 
-3. Chaos Engineering :
+### 3. Chaos Engineering :
+
 Read the paper and briefly explain what are the concrete experiments they perform, what are the requirements for these experiments, what are the variables they observe and what are the main results they obtained.  Speculate 
 
 The experiments they performed that they said the paper are
@@ -92,7 +95,7 @@ Variables to observe:
 - Data consistency metric
 - Error rate
 
-4. Formal specification in Web Assembly :
+### 4. Formal specification in Web Assembly :
 
 Selon les concepteurs de Web Aseembly, la sémantique formelle permet d'avoir un code plus propre et régulier, il est plus facile à implémenter.
 WebAssembly est prouvable grâce à sa sémantique formelle, il évite les comportements indéfinis.
@@ -102,5 +105,9 @@ Le code peut être vérifié, compilé et transformé en format Automate en un s
 Mais tout ceci ne remplace pas les tests. La sémantique formelle permet seulement de garantir que le comportement est défini et que l'exécution est sûre. Les tests eux vérifient que le programme respecte la spécification.
 
 
-5. Mechanising and Verifying :
+### 5. Mechanising and Verifying :
 
+Ici, on a une version mécanisée de WebAssembly par l'assistant de preuve Isabelle.
+Cela permet de prouver les propriétés essentielles, détecter les contradictions ou ambiguïtés dans les règles et démontrer que le système de type est sûr.
+Le type cheker et l'interpréteur sont vérifiés.
+La mécanisation a contribué à rendre WebAssembly plus sûre, en repérant des incohérences, des règles mal typées et des comportements non définis.