Karl Palmskog (Jul 01 2022 at 20:40): Karl Palmskog (Jul 01 2022 at 20:40):In the spirit of "proof assistants need not necessarily compete":
we have a HOL4+CakeML development on a language for describing and analyzing low-level information flow / side channels (think of leaking secrets just below ISA level): https://github.com/kth-step/mil - the language and its semantics could be translated to Coq quite easily (we use the Ott tool), so if anyone is interested in using such a language in Coq, would be happy to help make that happen. The pen-and-paper background is here.
Last updated: Sep 15 2024 at 13:02 UTC