Stream: Miscellaneous

Topic: Formalization of low level information flow


view this post on Zulip 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: Aug 19 2022 at 20:03 UTC