忘记密码   免费注册 查看新帖 | 论坛精华区

ChinaUnix.net

  平台 论坛 博客 认证专区 大话IT HPC论坛 徽章 文库 沙龙 自测 下载 频道自动化运维 虚拟化 储存备份 C/C++ PHP MySQL 嵌入式 Linux系统
最近访问板块 发新帖
查看: 967 | 回复: 2

Linux 基金会透露未来:Linux内核可能会引入形式验证 [复制链接]

论坛徽章:
135
2015年亚洲杯之日本
日期:2015-04-28 13:32:012015年亚洲杯之朝鲜
日期:2015-05-06 10:16:442015年亚洲杯之日本
日期:2015-05-06 10:21:342015年亚洲杯纪念徽章
日期:2015-05-13 17:16:442015亚冠之北京国安
日期:2015-05-13 17:18:292015亚冠之鹿岛鹿角
日期:2015-05-13 17:19:062015亚冠之德黑兰石油
日期:2015-05-27 16:47:402015亚冠之塔什干棉农
日期:2015-05-28 15:24:122015亚冠之卡尔希纳萨夫
日期:2015-06-01 13:52:392015亚冠之柏斯波利斯
日期:2015-06-04 17:37:292015亚冠之阿尔纳斯尔
日期:2015-06-16 11:31:202015亚冠之塔什干火车头
日期:2015-06-23 10:12:33
发表于 2017-06-27 12:56 |显示全部楼层
来源:太平洋电脑网

在北京举办的 LC3 大会 (LinuxCon + ContainerCon + CloudOpen)应该是全球最顶级的开源大会了,而这一为期两天的开源盛会过去几年在北美、欧洲和日本都举办过,而此次是其首次来到中国。就在同一天,Linux 发布了 4.12-rc6 的 release,而Linux 基金会在这次大会上也独家透露了一些未来 Linux 内核开发的新特性。

Linux 基金会的执行董事 Jim Zemblin 是本次大会的主持人,他同时也出席了本次大会的发布会,接受了中国媒体的专访,在19日上午 Linux Story 记者闻其详的访问中,Jim 透露,未来 Linux 内核可能会引入形式验证(维基百科链接),以获得更好的安全性,如果完成形式验证的话,将大大增加 Linux 在内核安全上的可信赖度,也有利于 Linux 对更多新特性的支持和未来长远发展。但是形式验证是一项艰巨的任务,我们估计 Linux 应该首先对某些相对独立的核心模块完成形式验证。

据悉,形式验证(Formal Verification)含义是根据某个或某些形式规范或属性,使用数学的方法证明其正确性或非正确性。同时逻辑形式验证是一个系统性的验证过程,它使用数学方法来验证设计在实现中是否得以贯彻。目前主要常用的形式验证软件包括 Coq / Isabelle / Metamath / TLA+ 等。

形式验证过程可以证明一个系统不存在某个 bug 或符合某些规范。而传统软件测试方法的局限在于,有限的测试用例无法覆盖几乎无限的状态空间,测试环境没有考虑到的例外状况往往会成为隐患,在生产环境中造成损失。测试用例再多,也无法保证系统不出现bug,然而对于一些关键应用场景,我们又非常需要一个没有bug的系统。“没有bug”是一个很难严格定义的概念,更现实的做法是尽力排除“特定类型的bug”。形式验证方法可以针对业务逻辑或者代码逻辑进行数学证明,证明一个系统符合特定的设计规范,证明系统不存在任何已知类型的bug,以及证明系统满足特定的功能属性。

形式验证方法有超过30年的历史。目前形式验证在芯片设计,云计算,操作系统,编译器,区块链等领域都有应用。

如果 Jim 透露的计划能够顺利实施,也许未来可以期待 Docker 之类的轻量级隔离实现跟传统虚拟化媲美的安全级别,这对 Linux 未来在云计算和容器方面的发展大有裨益,而 Docker 也将从 Linux 内核安全性的加强中获益,这也可能是 Linux 未来的发展方向的一部分。不过 Jim 同时也说,这是一个很困难的过程,目前还不能保证形式验证相关工作的具体时间表。





论坛徽章:
11
每日论坛发贴之星
日期:2016-06-10 06:20:00综合交流区版块每日发帖之星
日期:2016-06-10 06:20:00黑曼巴
日期:2016-06-08 11:29:1815-16赛季CBA联赛之同曦
日期:2016-06-07 17:47:2815-16赛季CBA联赛之山东
日期:2016-04-18 10:23:102016猴年福章徽章
日期:2016-02-18 15:30:3415-16赛季CBA联赛之吉林
日期:2016-01-28 09:34:15辰龙
日期:2014-10-14 14:33:48巨蟹座
日期:2014-04-23 11:27:44狮子座
日期:2014-02-26 16:08:29IT运维版块每日发帖之星
日期:2016-07-14 06:20:00
发表于 2017-06-28 16:41 |显示全部楼层
形式验证方法,嗯,这个概念很少听说。

论坛徽章:
4
天蝎座
日期:2014-05-20 14:18:39水瓶座
日期:2014-12-19 09:15:322015年迎新春徽章
日期:2015-03-04 10:01:442015年亚洲杯之阿联酋
日期:2015-05-04 10:00:13
发表于 2017-07-14 14:07 |显示全部楼层
这么牛的?
您需要登录后才可以回帖 登录 | 注册

本版积分规则

SACC2017购票8.8折优惠进行时

2017中国系统架构师大会(SACC2017)将于10月19-21日在北京新云南皇冠假日酒店震撼来袭。今年,大会以“云智未来”为主题,云集国内外顶级专家,围绕云计算、人工智能、大数据、移动互联网、产业应用等热点领域展开技术探讨与交流。本届大会共设置2大主会场,18个技术专场;邀请来自互联网、金融、制造业、电商等多个领域,100余位技术专家及行业领袖来分享他们的经验;并将吸引4000+人次的系统运维、架构师及IT决策人士参会,为他们提供最具价值的交流平台。
----------------------------------------
优惠时间:2017年8月2日前

活动链接>>
  

北京盛拓优讯信息技术有限公司. 版权所有 京ICP备16024965号 北京市公安局海淀分局网监中心备案编号:11010802020122
广播电视节目制作经营许可证(京) 字第1234号 中国互联网协会会员  联系我们:
感谢所有关心和支持过ChinaUnix的朋友们 转载本站内容请注明原作者名及出处

清除 Cookies - ChinaUnix - Archiver - WAP - TOP