克里姆林宫基地

克里姆林宫 Linux 视窗 KreMLin是一种将F *程序提取为可读C代码的工具。 如果F *程序针对讨论堆栈和堆的低级内存模型进行验证，则为否； 如果是一阶的； 如果它遵守某些限制（例如非递归数据类型），则KreMLin会将其转换为C。 了解KreMLin的最好方法是其正在进行的。 欢迎提出要求和反馈！ 对KreMLin执行的不同转换过程进行了技术概述，并且已经过时了。 这项工作已在纸上正式化。 我们声明将此类F *程序编译为C可以保留语义。 我们从Low *（F *的子集）开始，并将其语义与的Clight相关联。 概述了KreMLin以及我们的编译工具链的论文形式化 我们编写了20,000行低级F *代码，实现了记录层。 因此，KreMLin是的关键组成部分。 是我们的高度保证加密库，提供了许多用F *编写的加密原语； 这些原语具有内存安全性，功能正确性和一定程度的旁