EverCrypt 正在参加 2020 年度 OSC 中国开源项目评选,请投票支持!
EverCrypt 在 2020 年度 OSC 中国开源项目评选 中已获得 {{ projectVoteCount }} 票,请投票支持!
投票让它出道
已投票
EverCrypt 获得 2020 年度 OSC 中国开源项目评选「最佳人气项目」 !
EverCrypt 获得 2020 年度 OSC 中国开源项目评选「最佳人气项目」「最积极运营项目」 !
EverCrypt 获得 2020 年度 OSC 中国开源项目评选「最积极运营项目」 !
授权协议 Apache-2.0
操作系统 跨平台
软件类型 开源软件
开源组织
地区 不详
提 交 者 局长
适用人群 未知
收录时间 2019-04-09

软件简介

程序员都是凡人,但数学则是不朽的。通过让编程变得更数学化,计算机科学家希望能消除向黑客敞开大门的编程错误。研究人员在 GitHub 上发布了加密工具 EverCrypt,向这个目标迈出了一大步。就像证明毕达哥拉斯定理那样,他们能证明 EverCrypt 可完全避开多种黑客攻击

EverCrypt 没有采用常见的编程方法编写,而是利用了形式化验证。他们首先明确代码能做什么,然后证明只能这么做,排除了代码在特殊情况下偏离的可能性。

EverCrypt 始于 2016 年,是微软研究院项目 Project Everest 的一部分,当时加密库是许多软件的薄弱环节,存在大量 bug。EverCrypt 使用 F*(发音 F star)编程语言编写和验证,然后编译为 C(使用专用编译器 KreMLin 编译)和汇编语言的混合。

EverCrypt 支持的算法

EverCrypt 支持的许多算法仍在开发中。在即将发布的版本中,目标是:

  • fallback C versions for all algorithms
  • NIST P curves
  • AES-CBC
  • an up-to-date Ed25519
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

参考 https://www.solidot.org/story?sid=60154

展开阅读全文

代码

的 Gitee 指数为
超过 的项目

评论 (2)

加载中
现在国家大力推广国密算法,支持国密用的人就多了
2019/10/27 13:18
回复
举报
用SHA加密MD5,双重
2019/05/18 13:30
回复
举报
更多评论
暂无内容
暂无内容
暂无内容
2 评论
78 收藏
分享
OSCHINA
登录后可查看更多优质内容
返回顶部
顶部