近日，科大少年班校友、耶鲁大学计算机系教授邵中小组成功研发世界上第一个反黑客攻击操作系统CertiKOS。

CertiKOS具有极高的安全性和可靠性，采用了模块分层验证法（modular layered verification methods），拥有并发性，可同时在多个CPU内核上多线程运行。此外，该系统整合了形式验证，对无论是智能家电还是物联网设备都能起到防黑客攻击的保护作用。CertiKOS的高可信度操作系统内核，可在此基础上建立能免受网络攻击的信息物理系统（CPS,Cyber-Physical Systems）。CertiKOS的模块分层验证法还可被应用到除操作系统外的任何软件中。

邵中教授简介

邵中，毕业于江苏省常熟中学，1983年考入中国科学技术大学少年班，1987年获得中国科大本科生最高荣誉奖——郭沫若奖学金，1988年获得计算机科学系学士学位。同年被美国普林斯顿大学录取，1991年获得硕士学位，1994年获得博士学位。

1994年博士毕业后，邵中被聘为美国耶鲁大学计算机科学系助理教授，2000年被提为副教授，2003年7月起，他晋升为耶鲁大学计算机系正教授，此时他尚未度过自己的35周岁生日。现任中国科大－耶鲁高可信软件联合研究中心主任，曾获美国国家科学基金青年学者奖。

邵中教授擅长程序设计语言及编译系统、高可信软件及系统程序验证等领域的研究，是这些领域的国际学术带头人之一。他和他的学生研究开发了多种新颖的用于实现“带证明可信软件”(Certified Software) 的程序逻辑，类型系统，和验证技术，在国际最顶级会议（如PLDI, POPL, ICFP, LICS, CONCUR等）和杂志 (如TOPLAS, JFP, CACM等) 上发表论文80多篇，是同领域中世界上最有影响力的科研小组之一。近年来，他的研究重点集中在开发新的带证明可信软件的理论和技术，目标是为开发经过验证的大规模系统软件构建一种实用的基础平台。

附：英文新闻原文

CertiKOS: A breakthrough toward hacker-resistant operating systems

By William Weir

A team of Yale researchers has unveiled CertiKOS, the world’s first operating system that runs on multi-core processors and shields against cyber attacks, a milestone that the scientists say could lead to a new generation of reliable and secure systems software.

Led by Zhong Shao, professor of computer science at Yale, the researchers developed an operating system that incorporates formal verification to ensure that a program performs precisely as its designers intended — a safeguard that could prevent the hacking of anything from home appliances and Internet of Things (IoT) devices to self-driving cars and digital currency. Their paper on CertiKOS was presented at the 12th USENIX Symposium on Operating Systems Design and Implementation held Nov. 2-4 in Savannah, Ga.

Computer scientists have long believed that computers’ operating systems should have at their core a small, trustworthy kernel that facilitates communication between the systems’ software and hardware. But operating systems are complicated, and all it takes is a single weak link in the code — one that is virtually impossible to detect via traditional testing — to leave a system vulnerable to hackers.

One of the main breakthroughs of CertiKOS is that it supports concurrency, meaning that it can simultaneously run multiple threads (small sequences of programmed instructions) on multiple central processing unit (CPU) cores. This sets CertiKOS apart from other previously verified systems and allows CertiKOS to run on modern multi-core machines. The CertiKOS architecture is also designed to be highly extensible — that is, it can take on new functionalities and be used for different application domains.

Concurrency allows overlapped execution of multiple program threads, which makes it impossible to consider all circumstances and eliminate all cracks in the system via traditional testing. Many in the field have long believed that the complexity of such a system also makes formal verification of functional correctness problematic or prohibitively expensive.

“The construction of functionally correct systems software has been one of the grand challenges of computing since at least the mid-20th century,” said Anindya Banerjee, program director at the National Science Foundation (NSF), which funds the CertiKOS effort partly through its Expeditions in Computing program. “CertiKOS demonstrates that it is feasible and practical to build verified software that additionally provides evidence — through machine-checkable mathematical proofs — that it is functionally correct.”

In constructing the CertiKOS system, Shao and his team incorporate formal logic and new, layered deductive verification techniques. That is, they carefully untangle the kernel’s interdependent components, organize the code into a large collection of hierarchical modules, and write a mathematical specification for each kernel module’s intended behavior. The use of formal deductive verification to certify the system differs from the conventional method of checking a program’s reliability, in which the code writer tests the program against numerous scenarios.

“A program can be written 99% correctly — that’s why today you don’t see obvious issues — but a hacker can still sneak into a particular set-up where the program will not behave as expected,” Shao said. “The person who wrote the software worked with all good intentions, but couldn’t consider all cases.”

The CertiKOS verified operating system kernel is a key component of the Defense Advanced Research Agency’s (DARPA) High Assurance cyber Military Systems (HACMS) program, which is used to build cyber-physical systems that are provably free from cyber vulnerabilities.

“The HACMS team uses the virtualization capability provided by CertiKOS to separate trusted from untrusted components,” DARPA program manager Ray Richards said. “This is an important ability that allows us to effectively build cyber-resilient systems. In the world where cybersecurity is a growing concern, this resiliency is a powerful attribute that we hope will be widely adopted by system designers.”

Only in recent years would a system like CertiKOS be possible, since the proofs for a certified kernel are too big for any human to check. Powerful computer programs known as proof assistants have been developed within the last 10 years, however, that can automatically generate and check large formal proofs.

“This is amazing progress,” said Greg Morrisett, a leading expert on software security and dean of computing and information sciences at Cornell University. “Ten years ago, no one would predict that we could prove the correctness of a single-threaded kernel, much less a multi-core one. Zhong and his team have really blazed a spectacular trail for the rest of us.”

Andrew Appel, director of NSF’s DeepSpec consortium and a professor of computer science at Princeton, called CertiKOS “a real breakthrough,” noting that it can serve as a base for building highly secure systems from combinations of verified and untrustworthy components.

“But just as important, the modular layered verification methods used in CertiKOS will be applicable not just to operating systems, but to many other kinds of software,” Appel said.

英文新闻来源：耶鲁大学官方网站，点击Yale News

稿件来源：中国科大新创基金会