资料介绍
软件简介
程序员都是凡人,但数学则是不朽的。通过让编程变得更数学化,计算机科学家希望能消除向黑客敞开大门的编程错误。研究人员在 GitHub 上发布了加密工具 EverCrypt,向这个目标迈出了一大步。就像证明毕达哥拉斯定理那样,他们能证明 EverCrypt 可完全避开多种黑客攻击。
EverCrypt 没有采用常见的编程方法编写,而是利用了形式化验证。他们首先明确代码能做什么,然后证明只能这么做,排除了代码在特殊情况下偏离的可能性。
EverCrypt 始于 2016 年,是微软研究院项目 Project Everest 的一部分,当时加密库是许多软件的薄弱环节,存在大量 bug。EverCrypt 使用 F*(发音 F star)编程语言编写和验证,然后编译为 C(使用专用编译器 KreMLin 编译)和汇编语言的混合。
EverCrypt 支持的算法
EverCrypt 支持的许多算法仍在开发中。在即将发布的版本中,目标是:
Algorithm | C version | ASM version | Agile API |
---|---|---|---|
AEAD | |||
AES-GCM | ✔︎ (AES-NI + PCLMULQDQ) | ✔︎ | |
ChachaPoly | ✔︎¹ | ✔︎ | |
Hashes | |||
MD5 | ✔︎² | ✔︎ | |
SHA1 | ✔︎² | ✔︎ | |
SHA2 | ✔︎ | ✔︎ | |
SHA3 | ✔︎ | ||
Blake2 | ✔︎ | ||
MACS | |||
HMAC | ✔︎⁴ | ✔︎ | |
Poly1305 | ✔︎³ (+ AVX + AVX2) | ✔︎ (X64) | |
Key Derivation | |||
HKDF | ✔︎⁴ | ✔︎ | |
ECC | |||
Curve25519 | ✔︎ | ✔︎ (BMI2 + ADX) | |
Ed25519 | ✔︎⁵ | ||
Ciphers | |||
Chacha20 | ✔︎ | ||
AES128, 256 | ✔︎ (AES NI + PCLMULQDQ) | ||
AES CTR | ✔︎ (AES NI + PCLMULQDQ) |
¹: does not multiplex (yet) over the underlying Poly1305 implementation
²: insecure algorithms provided for legacy interop purposes
³: achieved via C compiler intrinsincs; no verification results claimed for the AVX and AVX2 versions whose verification is not complete yet
⁴: HMAC and HKDF on top of the agile hash API, so HMAC-SHA2-256 and HKDF-SHA2-256 leverage the assembly version under the hood
⁵: legacy implementation
- 现代电机控制威廉希尔官方网站 .课件下载ppt 0次下载
- 现代电机控制威廉希尔官方网站 .王成元 夏加宽版 0次下载
- 基于FPGA芯片的软硬件平台的使用 20次下载
- 基于区块链的智能机器人多传感信息加密控制方法 5次下载
- 可提高隐私数据安全性的可搜索加密方案 10次下载
- MSP430总结:为什么要加密,如何加密?资料下载 7次下载
- 单片机TEA加密是怎么加密的?资料下载 10次下载
- 结合硬件算法平台等的可调认证加密方案 4次下载
- 现代无线电实验说明 13次下载
- 一种改进的加密恶意流量检测方法 13次下载
- AES加密算法在电子系统中的优化和应用分析 12次下载
- 三重数据加密和高级加密标准基于PIC24和dsPIC30/33的讨论详细概述 8次下载
- 透明加密软件的特点及原理 0次下载
- CPU卡加密系统与M1加密系统 3次下载
- 空中无人平台视频图像加密算法研究 23次下载
- 加密狗是什么意思 加密狗怎么解除加密 1403次阅读
- 简单认识安全加密处理器 466次阅读
- 什么是光模块的写码加密? 1269次阅读
- 加密算法与非加密算法的区别 1671次阅读
- 区块链与加密货币有什么不同? 4102次阅读
- 基于以太坊平台建立的去中心化金融应用kyberNetwork解析 807次阅读
- 关于音视频加密防爬的威廉希尔官方网站 解析 1305次阅读
- 加密货币生态系统DAGNe威廉希尔官方网站 原理解析 1588次阅读
- 什么是私钥加密?私钥加密和公钥加密有何区别? 2.7w次阅读
- 加密货币风暴,现代加密数字货币面临的问题及解决方案 1859次阅读
- 常用的PHP加密函数有哪些?不可逆加密函数和可逆转加密函数概述 6517次阅读
- 一文读懂VSAN加密威廉希尔官方网站 2158次阅读
- 什么是非对称加密?非对称加密概念 2.1w次阅读
- 非对称加密算法有什么特点 2.2w次阅读
- 常见公钥加密算法有哪些 4.2w次阅读
下载排行
本周
- 1山景DSP芯片AP8248A2数据手册
- 1.06 MB | 532次下载 | 免费
- 2RK3399完整板原理图(支持平板,盒子VR)
- 3.28 MB | 339次下载 | 免费
- 3TC358743XBG评估板参考手册
- 1.36 MB | 330次下载 | 免费
- 4DFM软件使用教程
- 0.84 MB | 295次下载 | 免费
- 5元宇宙深度解析—未来的未来-风口还是泡沫
- 6.40 MB | 227次下载 | 免费
- 6迪文DGUS开发指南
- 31.67 MB | 194次下载 | 免费
- 7元宇宙底层硬件系列报告
- 13.42 MB | 182次下载 | 免费
- 8FP5207XR-G1中文应用手册
- 1.09 MB | 178次下载 | 免费
本月
- 1OrCAD10.5下载OrCAD10.5中文版软件
- 0.00 MB | 234315次下载 | 免费
- 2555集成电路应用800例(新编版)
- 0.00 MB | 33566次下载 | 免费
- 3接口电路图大全
- 未知 | 30323次下载 | 免费
- 4开关电源设计实例指南
- 未知 | 21549次下载 | 免费
- 5电气工程师手册免费下载(新编第二版pdf电子书)
- 0.00 MB | 15349次下载 | 免费
- 6数字电路基础pdf(下载)
- 未知 | 13750次下载 | 免费
- 7电子制作实例集锦 下载
- 未知 | 8113次下载 | 免费
- 8《LED驱动电路设计》 温德尔著
- 0.00 MB | 6656次下载 | 免费
总榜
- 1matlab软件下载入口
- 未知 | 935054次下载 | 免费
- 2protel99se软件下载(可英文版转中文版)
- 78.1 MB | 537798次下载 | 免费
- 3MATLAB 7.1 下载 (含软件介绍)
- 未知 | 420027次下载 | 免费
- 4OrCAD10.5下载OrCAD10.5中文版软件
- 0.00 MB | 234315次下载 | 免费
- 5Altium DXP2002下载入口
- 未知 | 233046次下载 | 免费
- 6电路仿真软件multisim 10.0免费下载
- 340992 | 191187次下载 | 免费
- 7十天学会AVR单片机与C语言视频教程 下载
- 158M | 183279次下载 | 免费
- 8proe5.0野火版下载(中文版免费下载)
- 未知 | 138040次下载 | 免费
评论
查看更多