Cryptol

2022年11月23日 (三) 14:41的最后版本

Cryptol

[编辑] 简介

Cryptol 是用于在 C 和 VHDL 中设计安全密码系统的加密语言，使用 Haskell 语言编写。

[编辑] 功能

Cryptol 第2版解释器包括一个 :check 命令，该命令针对随机生成的测试向量（test vectors）测试用 Cryptol 编写的谓词（类似 QuickCheck 风格）。还有一个 :prove 命令，用于调用 SMT 求解器，如 Yices Z3 或 CVC4 以证明所有可能的输入的谓词。

[编辑] 指南

[编辑] 项目

• Cryptol @ GitHub

[编辑] 文档

• Verified Cryptographic Code for Everybody

[编辑] 图集

• 

  Cryptol REPL

[编辑] 链接

• Cryptol官网
• Galois, Inc.