<dd id="yzu3f"><tr id="yzu3f"><kbd id="yzu3f"></kbd></tr></dd>

              安基网 首页 资讯 安全报 查看内容

              利用数学工具写出黑客无法攻陷的软件

              2019-4-12 12:17| 投稿: xiaotiger |来自: 互联网


              免责声明:本站系公益性非盈利IT技术普及网,本文由投稿者转载自互联网的公开文章,文末均已注明出处,其内容和?#35745;?#29256;权归原网站或作者所有,文中所述不代表本站观点,若有无意侵权或转载不当之处请从网站右下角联系我们处理,谢谢合作!

              摘要: 程序员是人类,但数学是不朽的。通过使编程更具数学性,计算机科学家希望消除可能被黑客利用、泄露数字机密并对现代社会造成普遍困扰的程序bug。现在,随着EverCrypt(一款数字?#29992;?#24037;具)的发布,一组计算机科学家朝着宏伟目标迈出了重要的一步。研究人员能够证明——证明毕达哥拉斯定理的那种证明——对 ...

              程序员是人类,但数学是不朽的。通过使编程更具数学性,计算机科学家希望消除可能被黑客利用、泄露数字机密并对现代社会造成普遍困扰的程序bug。

              现在,随着EverCrypt(一款数字?#29992;?#24037;具)的发布,一组计算机科学家朝着宏伟目标迈出了重要的一步。研究人员能够证明——证明毕达哥拉斯定理的那种证明——对于黑客用来攻陷以往程序的主要手段,最新的安全工具是完全无懈可击的。“我们的意思是,我们通过数学方法证明,我们的代码不会受到这种攻击。”巴黎Inria的计算机科学家Karthik Bhargavan表示。

              EverCrypt程序并非是按照常见的方式编写。通常,程序员团队先创建他们希望能够满足某些需求的软件。完成后,他们会测试。如果它顺顺当当地完成了目标,并且不会出现预期外的行为,程序员就得出结论:该软件能用了。

              然而,bug通常只出现在极端的“边界情况corner cases?#27605;隆?#36817;年来,许多最具?#33529;?#24615;的黑客工具都利用了极端情况。

              相比之下,卡内基梅隆大学计算机科学家Bryan Parno和同事已经明确限定了他们程序的功能,然后证明了它的行为真的被局限在已知的?#27573;?#20869;,排除了在特殊情况下代码可能以意想不到的方式偏离正轨的可能性。这种策?#21592;?#31216;为“?#38382;?#39564;证”。

              因为完全定义复杂软件系统(如网络浏览器)的功能几乎是不可能的,所以研究人员转而关注那些既重要又适合数学定义的程序。 EverCrypt是处理密码或私人信息编码和解码的软件库。这些?#29992;?#24211;具有天生的数学性。它们涉及算术与素数和对规?#37117;?#20309;对象(如椭圆曲线)的操作。定义?#29992;?#24211;并不是一件容易的?#38534;?/p>

              EverCrypt的开发?#21152;?016年,作为Project Everest的一部分,后者是由微软研究院主持的项目。当时——现在仍然如此——?#29992;?#24211;是许多软件应用程序中的一个软肋。它们运?#35874;?#24930;,拖累了所属应用程序的整体性能,?#39029;?#28385;bug。

              创建EverCrypt的主要挑战是发明出一款一体化的开发平台,可以容纳研究人员为经过验证的?#29992;?#24211;添加的所有不同属性。该平台既需要C++这样的传统编程语言的能力,又能如Isabelle和Coq这样的证明辅助程序一样提供逻辑语法和结构——数学家们已经使用了这两款软件很多年。当EverCrypt项?#31185;?#21160;时,还并没有这样的一体化平台,因此他们自己开发了一种——名为F *的编程语言。它把数学和编程放到了平等的地位。

              “我们将这些事情统一到一个连贯的框架中,这样就可以减少编写程序和数学证明之间差异,”Bhargavan说,“你可以像软件开发人员一样写代码,但同时你也可以写数学证明。”

              他们证明,EverCrypt并没有可供黑客利用的bug,如缓冲区溢出。?#23548;噬希?#21487;以证明它排除了对所有可能的极端情况的敏感性。他们还证明,EverCrypt?#30475;?#37117;能获得正确的数学?#29992;?#32467;果——它从不执?#20889;?#35823;的运算。

              但EverCrypt最引人注目的?#20449;?#26469;自对完全不同方向上的安全弱点——?#34987;?#20154;通过观察程序如何操作来推断?#29992;?#28040;息的内容时,就会出现的情况——的防护。

              例如,有经验的观察者可能知道?#29992;?#31639;法为值赋予“0”时,程序的运行速度稍快,而在向值添加“1”时稍慢。通过测量算法?#29992;?#28040;息所花费的时间量,观察者可以判断出消息的二进制表示是否包含更多的0或1——并最终推断出完整的消息。

              ?#25353;?#32479;?#29992;?#31639;法的原理本身,或者实现算法的方式,正在泄露你的信息。”Bhargavan说。这种“旁道攻击”是近年来?#22797;?#26368;臭名昭着的黑客事件的幕后推手,其中包括?#20197;?3袭击。研究人员证明,EverCrypt绝不会被利用以上述方式泄露信息。

              虽然EverCrypt可以免疫许多攻击类型,但它并不意味着绝对安全的软件时代已然来临。Protzenko指出,人们总是会想出未知的方式来利用程序漏洞,无法证明EverCrypt是永远安全的。

              此外,即使是经过验证的?#29992;?#24211;也必须与许多其他软件(如操作系统和许多常见的桌面应用程序)协同工作,这些软件通常是未经验证的,并且可能在可预见的未来也不会通过?#38382;?#39564;证。

              由于未经验证的协同应用可能会抵消?#29992;?#24211;的安全性,Project Everest希望使用尽可能多地使用经过验证的软件来配合EverCrypt。该计划的首要目标是完成安全超文本传输协议(HTTPS)的全面验证,该协议可保护大多数网络通信的安全。

              本文译自 quantamagazine,由译者 majer 基于创作共用协议(BY-NC)发布。



              小编推荐:欲学习电脑技术、系统维护、网络管理、编程开发和安全攻防等高端IT技术,请 点击这里 注册账号,公开课频道价值万元IT培训教程免费学,让您少走弯路、事半功倍,好工作升职加薪!

              本文出自:https://www.toutiao.com/a6678803355495563787/

              免责声明:本站系公益性非盈利IT技术普及网,本文由投稿者转载自互联网的公开文章,文末均已注明出处,其内容和?#35745;?#29256;权归原网站或作者所有,文中所述不代表本站观点,若有无意侵权或转载不当之处请从网站右下角联系我们处理,谢谢合作!


              鲜花

              ?#24080;?/a>

              雷人

              路过

              鸡蛋

              相关阅读

              最新评论

               最新
              返回顶部
              十一选五奖金对照表