FStarLang/karamel

## KaRaMeL | Linux | |---------| [](https://github.com/FStarLang/karamel/actions/workflows/ci.yml) KaRaMeL（原名 KReMLin）是一个将 F\* 程序提取为可读 C 代码的工具：K&R 与 ML 的结合！ 如果该 F\* 程序能够通过与栈和堆相关的低层内存模型验证；如果它是一阶的；并且如果它遵循某些限制（例如非递归数据类型），那么 KaRaMeL 就能将其转换为 C 代码。 了解 KaRaMeL 的最佳方式是阅读其正在不断完善中的[教程](https://fstarlang.github.io/lowstar/html/)。欢迎提交 Pull request 和反馈！ - [DESIGN.md](DESIGN.md) 提供了 KaRaMeL 所执行各项转换过程的技术概述，不过内容略有滞后。 这项工作已在论文中形式化。我们指出，将此类 F\* 程序编译为 C 语言能够保留其语义。我们从 F\* 的一个子集 Low\* 出发，并将其语义与 [CompCert](http://compcert.inria.fr/) 的 Clight 联系起来。 - [ICFP 2017 论文] 提供了 KaRaMeL 的概述，以及我们编译工具链的论文形式化描述。 我们已经编写了 120,000 行 Low\* 代码，实现了 [TLS 1.3](https://tlswg.github.io/tls13-spec/) 记录层。因此，KaRaMeL 是 [Project Everest](https://project-everest.github.io/) 的关键组件。 - [HACL\*]，我们的高保障密码学库，提供了许多用 F\* 编写的密码学原语；这些原语具备内存安全性、函数正确性以及一定程度的抗侧信道能力——它们通过 KaRaMeL 提取为 C 代码。 ## 试用 KaRaMeL KaRaMeL 需要 OCaml (>= 4.10.0)、OPAM 以及最新版本的 GNU make。 **关于 GNU make：** 在 OSX 上，这可能需要您通过 Homebrew 安装最新版本的 GNU make，并调用 `gmake` 而不是 `make`。 **关于 OCaml：** 通过您的包管理器安装 OPAM，然后执行： `$ opam install ppx_deriving_yojson zarith pprint "menhir>=20161115" sedlex process fix "wasm>=2.0.0" visitors ctypes-foreign ctypes uucp` 接下来，请确保您拥有最新版本的 F\*，无论是通过二进制包安装的，还是通过运行 `make` 编译构建的。`fstar.exe` 可执行文件应该位于您的 PATH 中，或者您可以设置变量 `FSTAR_EXE` 来指定其位置。 要构建，只需在此目录下运行 `make`。 **注意：** 在 OSX 上，如果您安装了 `greadlink`（通过 `brew install coreutils` 安装），KaRaMeL 运行起来会更顺畅。 如果您拥有正确版本的 F\*，并且 `fstar.exe` 位于您的 `PATH` 中，那么您可以通过执行 `make test` 来运行 KaRaMeL 测试套件。 ## 通过 OPAM 安装 KaRaMeL 也可通过 OPAM 获取，只需运行 `opam install karamel`。 如果您通过 OPAM 使用 `opam pin add fstar --dev-repo` 安装了最新版本的 F\*，您也可以通过运行 `opam pin add karamel --dev-repo` 来安装最新版本的 KaRaMeL。 如果遇到问题，请提交 Bug！ ## 文档 `--help` 标志包含了大量有用的信息。 ``` $ ./krml --help ``` ## 许可证 KaRaMeL 基于 [Apache 2.0 许可证] 和 MIT 许可证发布；有关更多详情，请参阅 `LICENSE-*`。

标签：CompCert, F*语言, HACL*, KaRaMeL, KReMLin, OCaml, OPAM, Project Everest, TLS 1.3, Web安全扫描, 云安全监控, 代码提取工具, 代码生成, 低级代码, 内存安全, 函数式编程, 密码学, 形式化验证, 手动系统调用, 渗透测试工具, 漏洞数据库, 程序转换, 编译优化, 编译器, 语义保持, 静态分析