硬核观察 #820 英伟达采用形式验证来验证软件安全性

英伟达采用形式验证来验证软件安全性

英伟达软件安全副总裁说，“面向测试的软件验证对安全来说根本不起作用，你可以对提供给用户的功能的质量有一个衡量标准，但对于安全问题，就没有什么作用，……很难知道你是否已经完成了。”幸运的是，有可能用数学方法证明你的代码的行为与它的规范精确一致。这个过程被称为“形式验证”。英伟达采用软件形式验证行业解决方案 SPARK 来证明软件的安全性。在几年前进行过概念验证后，现在许多英伟达产品在使用 SPARK 组件发布。

消息来源：AdaCore

老王点评：形式验证是个好方法，但是不是那么容易掌握和推行。

JavaScript、Java、Python、Kotlin 和 Rust 开发者增长惊人

根据 SlashData 去年夏天从 163 个国家的 26000 多名开发者调查统计而成的第 23 期《开发者国家报告》，JavaScript 仍然是最大的编程语言社区，全球估计有 1960 万开发者每天都在使用 JavaScript；在过去的两年里，Java 社区的规模已经从 830 万增加到 1650 万，而同期开发者只增加了 50%；Python 在过去两年中增加了约 800 万新的开发人员；Kotlin 和 Rust 社区的规模在过去两年里都翻了一番。

消息来源：ZDNet

老王点评：开发人员越来越倾向于使用主流开发工具，所以流行的越发流行，但是这样就会扼杀一些创新。

密码学家建议考虑非晶格的后量子密码算法

目前许多密码学系统的安全性是基于大数的因数分解的，但因数分解的一个怪癖使其容易受到量子计算机的攻击。因此人们对上世纪 90 年代提出的“晶格密码学”寄予厚望，美国 NIST 选择的四个后量子密码学标准有三个采用晶格密码学。RSA 算法名称中的 S，Adi Shamir 对此表示担忧，“从某种意义上说，我们是把所有鸡蛋放在同一个篮子里”。今年夏天早些时候，一个有前途的后量子密码学方案不是用量子计算机，而是用一台普通的笔记本电脑破解的。

消息来源：Slashdot

老王点评：确实如此，只有一种抗量子的密码理论，很难说会不会被发现潜在的弱点。