-
徐令予:攻不破、摧不垮、毒不侵的电脑怎样炼成?
关键字: 勒索病毒今日,形式化方法的研究人员的目标也变得更为现实。在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,每日阅读趣味文章。
-
本文仅代表作者个人观点。
- 请支持独立网站,转发请注明本文链接:
- 责任编辑:孙武
-
“若这么干,就能连通中国,拥有一条泛亚铁路” 评论 12“和谈应基于当下事实,泽连斯基已失合法性” 评论 160“美国想要中国大陆和台湾对抗,东盟没必要卷入” 评论 143习近平考察山东:努力成为北方地区经济重要增长极 评论 33联大通过争议性决议,武契奇:感谢中俄投下反对票 评论 215最新闻 Hot
-
“和谈应基于当下事实,泽连斯基已失合法性”
-
“全球科技巨头都是中国和美国的,这太疯狂了!”
-
“与中国比”?印外长寻求扩大对中亚、中东和非洲影响力
-
美军回应:正关注印太地区“所有活动”
-
俄安全局局长确认:乌军方情报部门与此案有直接关联
-
“普京希望以当前战线谈停火,西方不回应就继续打”
-
为这事,以色列痛批德国:许多人都需检查自己的道德准则
-
“巴方赔偿方案出炉:每人51.6万美元”
-
“美国想要中国大陆和台湾对抗,东盟没必要卷入”
-
“香港女警或入选第四批预备航天员载荷专家”
-
法国酒商不满欧盟对华政策:别连累我们
-
联大通过争议性决议,武契奇:感谢中俄投下反对票
-
“欧盟专员威胁我,小心成为下一个菲佐”
-
以色列杠上西班牙:绝对忍不了
-
菲防长拒绝评论解放军演习:台海局势属于中国内政
-
直击演练现场:轰炸机前出岛链,实施模拟打击
-