clarifies whether we consider taint escaping the current thread or not in the taint analysis (#15)

Author: ArquintL

claims/claim2/claim.md

@@ -1,4 +1,9 @@
 # Claim 2 - I/O Independence for SSM Agent
-As described in Sec. 5.1.2, we successfully execute a taint analysis on the entire SSM Agent codebase to prove that all I/O operations within the APPLICATION are independent of protocol-relevant secrets.
+As described in Sec. 5.1.2, we successfully execute a taint analysis on the entire SSM Agent codebase if we ignore taint escaping the current thread.
+We use a taint analysis to establish I/O independence, which states that all I/O operations within the APPLICATION are independent of protocol-relevant secrets.
 
-`run.sh` supports this claim by executing the taint analysis. The taint analysis uses the configuration `ssm-agent/argot-proofs/argot-config-agent.yaml`, in particular the configuration under key `dataflow-problems`. This configuration specifies that the analysis considers implicit flows, that the `GenerateKey` function in the `crypto/elliptic` package is a source of taint, and all functions that are treated as sinks. Since the taint analysis errors if taint flows from the source to any sink, successful execution of the analysis proves that there are no taint flows.
+`run.sh` supports this claim by executing the taint analysis. The taint analysis uses the configuration `ssm-agent/argot-proofs/argot-config-agent.yaml`.
+`use-escape-analysis: false` instructs the taint analysis to ignore taint escaping the current thread.
+The configuration under key `dataflow-problems` specifies that the analysis considers implicit flows, that the `GenerateKey` function in the `crypto/elliptic` package is a source of taint, and all functions that are treated as sinks.
+The taint analysis errors if a flow of taint from the source to any sink is detected.
+We use the taint analysis for checking I/O independence by configuring protocol secrets as sources of taint and all I/O operations in the APPLICATION and protocol-irrelevant I/O operations in the CORE as sinks.

claims/claim2/expected.md

@@ -1,4 +1,4 @@
-The script terminates successfully (exit code 0) indicating that the taint analysis succeeded and its output ends similarly to the following:
+The script terminates successfully (exit code 0) indicating that the taint analysis succeeded, and its output ends similarly to the following:
 
 ```
 [INFO].ssm-session-worker Taint analysis took 9.6177 s

claims/claim6/claim.md

@@ -1,4 +1,6 @@
 # Claim 6 - I/O Independence for Diffie-Hellman
 As described in Sec. 5.2, we successfully execute a taint analysis on the Diffie-Hellman codebase to prove that all I/O operations within the APPLICATION are independent of protocol-relevant secrets.
 
-`run.sh` supports this claim by executing the taint analysis. The taint analysis uses the configuration `dh/argot-proofs/argot-config-dh.yaml`, in particular the configuration under key `dataflow-problems`. This configuration specifies that the analysis considers implicit flows, that the `parsePrivateKey` and `createNonce` functions are sources of taint, and all functions that are treated as sinks. Since the taint analysis errors if taint flows from the source to any sink, successful execution of the analysis proves that there are no taint flows.
+`run.sh` supports this claim by executing the taint analysis. The taint analysis uses the configuration `dh/argot-proofs/argot-config-dh.yaml`, in particular the taint analysis considers taint escaping the current thread.
+The configuration under key `dataflow-problems` specifies that the analysis considers implicit flows, that the `parsePrivateKey` and `createNonce` functions are sources of taint, and all functions that are treated as sinks.
+Since the taint analysis errors if taint flows from the source to any sink, successful execution of the analysis proves that there are no taint flows, and, because of our configuration that I/O independence holds.