硬核观察 #820 英伟达采用形式验证来验证软件安全性
• 英伟达采用形式验证来验证软件安全性 • JavaScript、Java、Python、Kotlin 和 Rust 开发者增长惊人 • 密码学家建议考虑非晶格的后量子密码算法
安全 编程语言 量子密码
• 英伟达采用形式验证来验证软件安全性 • JavaScript、Java、Python、Kotlin 和 Rust 开发者增长惊人 • 密码学家建议考虑非晶格的后量子密码算法
![](/data/attachment/album/202211/14/171325wh1xp2kj0mc13mzl.jpg)


![](/data/attachment/album/202211/14/171335rq9ur5uzzuu9ttgl.jpg)


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


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



> 
> **[消息来源：AdaCore](https://blog.adacore.com/nvidia-security-team-what-if-we-just-stopped-using-c)**
> 
> 
> 



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


![](/data/attachment/album/202211/14/171346w1qw21q1m2p7nn2n.jpg)


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


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



> 
> **[消息来源：ZDNet](https://www.zdnet.com/article/software-development-is-evolving-and-so-is-what-developers-are-interested-in/)**
> 
> 
> 



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


![](/data/attachment/album/202211/14/171424sjere5d9erq4q435.jpg)


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


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



> 
> **[消息来源：Slashdot](https://it.slashdot.org/story/22/11/13/2042250/cryptographys-future-will-be-quantum-safe-heres-how)**
> 
> 
> 



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

