程序员都是凡人，但数学则是不朽的。通过让编程变得更数学化，计算机科学家希望能消除向黑客敞开大门的编程错误。研究人员在 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
-
我正在更新一个密码加密实用程序，从完全自带的东西到一个围绕Jasypt和Bouncy Castle构建的。实用程序加密密码；然后，加密的字符串被补丁到属性文件中，并由Grails应用程序回读和解密。 我编写了一个Java命令行实用程序来加密密码。相关的Java代码是：
-
多平台支持 Mpx支持在多个小程序平台中进行增强，目前支持的小程序平台包括微信，支付宝，百度，qq和头条，不过自2.0版本后，Mpx支持了以微信增强语法为base的跨平台输出，实现了一套业务源码在多端输出运行的能力，大大提升了多小程序平台业务的开发效率，详情可以查看template增强特性 不同平台上的模板增强指令按照平台的指令风格进行设计，文档和代码示例为了方便统一采用微信小程序下的书写方式。
-
问题内容： py2exe很棒，每当我想打包一个要在Windows系统上运行的python程序时，我都会使用py2exe。 我的问题是，是否可以使用等效工具在Windows上打包程序，但是可以在Linux上运行？ 问题答案： 好的，我已经做到了。这有点hacky，但是对于我的用例来说效果很好。 要点是使用ModuleFinder查找所有导入的模块，过滤掉所有系统模块，编译并压缩它们。 不幸的是，我的
-
问题内容： 简而言之：在iPhone和Android版本之间共享/重用代码的最有效方法是什么？ 我认为最常见的两种情况是： 空白计划新项目，提前知道每个设备上都需要运行大量可重用的逻辑。 现有的iPhone代码库，可将C，C ++和Objective-C移植到Android NDK或其他方式。 当然，在完美的世界中，所有应用程序都只会插入神奇的云中，而所有可重用的逻辑都将出现在Google App
-
我需要在我的应用程序中为不同的标签指定不同的FontFamily。我需要使用默认字体（如Android的Roboto和iOS的Helvetica）及其修改（如轻、中、粗）。据我所知，我应该使用Roboto-Light和Helvetica-Light来获得字体的轻版本（中号和粗体相同）。除了这个需求之外，我还需要在XAML中设置字体（如文档中所描述的），所以我最终得到了以下代码 然而，在Androi
-
作为第三代数据统计和分析平台，诸葛实现了对用户的实名（实账号）分析，并主张互联网产品分析以用户为中心的分析思想并提供了一系列方法论。对用户的唯一标识来源于企业自身数据库对用户的唯一识别符，也即诸葛底层数据采集是以用户为中心的采集，我们提供了跨平台分析版本， 满足企业以用户为中心的整体的分析需求，不同平台相同业务价值下的用户完整的故事解读(例如：分析电商的用户在PC端浏览产品，在移动端支付的转化率)
-
说明 由于在跨端开发中，必不可少的会遇到不同端需要有不同实现的情况。参考滴滴chameleon中的多态，megalo中实现了类似的跨平台兼容方案。需要使用时，请保证@megalo/target的版本号大于或等于0.7.2。 js的跨平台兼容 megalo中下面两种形式的引用会被特殊处理： [path-to-name]/[name]/index.mpjs [path-to-name]/[name]
-
问题内容： 我想开发一个跨平台的应用程序。 Java是跨平台的吗？我的意思是，我可以在Windows中开发Java应用程序并在Mac OS X和Linux中使用它吗？ 如果是，怎么办？ 我发现用Java编写的应用程序有两个安装文件，一个用于Windows，另一个用于Mac。 这使我感到困惑。 任何插图或建议将不胜感激。 问题答案： Java是跨平台的吗？ 从某种意义上说，Java是跨平台的， 即已