-
徐令予:攻不破、摧不垮、毒不侵的电脑怎样炼成?
关键字: 勒索病毒今日,形式化方法的研究人员的目标也变得更为现实。在20世纪70年代和80年代初期,这些研究人员试图创建可以验证的计算机系统,一个从硬件电路到软件程序的完整系统。如今大多数研究人员侧重于验证系统中较小但特别脆弱或关键的部分,如操作系统和加密协议。
“我们并不声称我们将证明整个系统是正确的,每一点都百分之百的可靠,从上至下直到电子电路的水平。”微软研究院的计算机科学家Jeannette Wing指出:“这些做法是荒谬的。我们更清楚我们能做什么,不能做什么。”
HACMS项目显示了如何通过计算机系统分区隔离以达到总体的安全保证。该项目的第一个目标是创造一个无法入侵的娱乐级四轴飞行器。运行该飞行器的商业软件是一个整体,这意味着如果攻击者突破一点,他就可以控制整个软件。在接下来的两年中,HACMS团队将四轴飞行器的任务控制计算机中的代码分区隔离。
该团队还重新制定了软件架构,使用了被HACMS项目经理凯瑟琳·费舍尔称之为“高保证构建块”的技术,这是一种让程序员证明其代码正确无误的工具。其中一个经过验证的构建块可以保证在某个分区内具有访问权限的操作者无法升级越界进入其他分区。
高保证网络军事系统(HACMS)项目主管 凯瑟琳·费舍尔
在四轴飞行器取得经验之后,HACMS程序员在“小鸟”军用无人直升机上安装了这个分区隔离软件。在测试中,他们提供了黑客团队进入无人直升机的某一分区,例如摄相机控制分区,但并不是核心功能分区。在无情的数学公式面前,黑客被死死地卡住在一个分区中无法乱说乱动。“他们以机器检查的方式证明,黑客不能脱离分区,这毫不奇怪,他们就是不能。”凯瑟琳·费舍尔说:“这与定理是一致的,试验也证明了这一点。”
为了帮助非专业人员了解分区隔离技术的基本原理,让我们回顾一下上世纪中国绝密军工厂的管理,这类军工厂不仅门卫森严,而且内部分成密级不同的独立车间,人员不得互相来往。每个产品又必经多个车间加工生产。一个间谍(黑客)进入工厂并混进某个车间已经非常不易,他下足工夫取得车间主任的信任或许能获得某种特权,但他最多只能在一个车间中活动,他对整个产品的认识和控制是十分有限的,因为任何试图跨越车间界限的行为会被严格的限制,而且其真实身份会立刻受到特别调查。计算机系统的分区隔离技术与绝密军工厂的管理方式有着某种程度的类同。
近年来,计算机硬件性能的飞速进步也为计算机系统的分区隔离技术提供了物质基础,今日强大的中央处理器能力和海量的内存空间完全可以支持系统的分区运行管理。
在“小鸟”无人直升机测试之后的一年,DARPA正努力将HACMS项目的工具和技术应用于其他军事技术领域,如卫星和无人自动驾驶车队。
为了捍卫互联网的安全,形式化方法的研究人员正在推动更加雄心勃勃的计划。DeepSpec合作项目力图将过去十年中已经成功通过形式化验证的许多小型模块进行组合,以构建一个经过完全形式化验证的端到端系统,如Web服务器。
在微软的研究部门,软件工程师正在进行两项雄心勃勃的形式化验证项目。第一个名为珠穆朗玛峰,这是创建一个经过形式化验证的HTTPS版本,新的协议可以有效地保护被称之为“互联网的阿喀琉斯之踵”的网络浏览器。第二个是为复杂的网络物理系统(如无人机)制定形式化验证规范,这里的挑战可能更为严峻。无人机飞行涉及到机器学习,以及在连续的环境数据流中进行概率决定,如何对不确定性进行推理并制定形式化规范是极大的挑战。但在过去的十年中,软件工程的形式化方法已经有了长足的进步,从事该项研究的科学家们对未来持有谨慎乐观的态度。
[1]形式化方法(Formal Method)是基于严密的、数学上的形式机制的计算机系统研究方法,该知识体系中有6个主要领域,分别为:
① 基础(Foundations);
② 形式化规格(Formal specification paradigms);
③ 正确性验证及演算(Correctness, verification and calculation);
④ 形式化语义(Formal semantics);
⑤ 可执行规范支持(Support for executable specification);
⑥ 其他(Other Topics)。
本文系观察者网独家稿件,文章内容纯属作者个人观点,不代表平台观点,未经授权,不得转载,否则将追究法律责任。关注观察者网微信guanchacn,每日阅读趣味文章。
-
本文仅代表作者个人观点。
- 请支持独立网站,转发请注明本文链接:
- 责任编辑:孙武
-
最新闻 Hot
-
欧核中心理事会主席:我有信心中国科学家能做到
-
“俄计划建新管道,经哈萨克斯坦向中国输送天然气”
-
他又来:美国连胡塞都搞不定,怎么让盟友放心搞定中国
-
历史性一幕!iPhone在华市场份额跌出前五
-
加沙民众上街庆祝,结果以色列说…
-
44岁男子穿裙子戴假发只为逃出乌克兰,被抓现行
-
一驻韩美军在俄被捕,“涉盗窃和殴打女性”
-
普京下令“核武演习”,美方回应
-
3个月后米莱终于回应:岛在他们手上,不把这当挑衅
-
“欧盟工具箱里没有美国式TikTok禁令,他们有自己的方式”
-
地面进攻在即?以军疏散拉法平民,哈马斯警告“后果”
-
中法欧领导人三方会晤结束
-
“我明确一点,不建议对华保持距离,我们需要中国人”
-
“五一”近3亿人次出游,较2019年同期增长28.2%
-
欧盟又挑争端?点名上汽、比亚迪、吉利,或抬高关税
-
问界回应山西M7车祸四大疑问:事发车速超过AEB工作范围
-