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

硬核观察 #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

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