github/Picus
1
1
Fork 0
mirror of https://github.com/Veridise/Picus.git synced 2026-04-19 03:00:11 -04:00
Code Issues Packages Projects Releases Wiki Activity

readme: fix math mode not rendered correctly

Browse Source
This commit is contained in:
Sorawee Porncharoenwase
2023-08-21 10:38:52 -07:00
committed by sorawee
parent 65f0ebe2dc
commit aa569bc26e
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
README.md
View File

@@ -193,7 +193,7 @@ A common way to mitigate the above issues is to split a big circuit into smaller
If a big target is too difficult to verify all at once fully automatically (which is the case for many real-world circuits), it is possible to do a semi-automatic way by manually tearing the circuits into pieces and perform automatic verification for each piece of them. If each piece can be verified successfully, this means the whole circuit is properly constrained. If all queries to the tool return `safe`, the overall result is also safe. If any query returns `unsafe` or `unknown` then the overall result is `unknown` since local unsafe cases could (but not always) lead to global vulnerability (since other parts of the circuit could have fixed the issues).
In some difficult cases where a template is very complicated -- e.g., a crypto hashing function -- and it is already difficult to verify the hash function itself, but supposing it is correct, it is possible to manually rewrite this difficult template into a relatively simple one with the same output domain to keep the computation easy for verification.
For example, suppose there is a circuit that is composed by `f(g(h(x)))` and `h(x)` is difficult to verify and blocking the remaining steps. But it is known that `h(x)` is definitely safe and the output domain of `h(x)` is known (let's say it is $out_h(x)$), it is possible to replace `h(x)` with a variable $y$ where $y \in out_h(x)$. By doing this, the semantics of the full circuit is preserved but the computation load for verification is reduced. Rewriting `h(x)` needs to be done carefully if there are more constraints applied on it, e.g., `a(b(h(x)))` -- basically the rewriting should not be breaking the semantics of the remaining part of circuit, or at least not under-approximating their relations -- that being said, if the circuit is rewritten to cover a larger variable space and can still verify it, it is ok.
For example, suppose there is a circuit that is composed by `f(g(h(x)))` and `h(x)` is difficult to verify and blocking the remaining steps. But it is known that `h(x)` is definitely safe and the output domain of `h(x)` is known (let's say it is $`out_h(x)`$), it is possible to replace `h(x)` with a variable $y$ where $y \in out_h(x)$. By doing this, the semantics of the full circuit is preserved but the computation load for verification is reduced. Rewriting `h(x)` needs to be done carefully if there are more constraints applied on it, e.g., `a(b(h(x)))` -- basically the rewriting should not be breaking the semantics of the remaining part of circuit, or at least not under-approximating their relations -- that being said, if the circuit is rewritten to cover a larger variable space and can still verify it, it is ok.
Note that these two options can be used to prove the correctness of the circuit. If there is indeed a bug there, then other approaches are needed to excavate the counter-example (something like an attack vector). When these two options say a circuit is `safe` then it is definitely `safe` (given that the rewrite is correct), but when they say a circuit is `unsafe`, it may not necessarily be `unsafe` since the variable space is over-approximated-- another semi-automatic way is needed to construct the counter-example.