Name
Abstract | ||
|---|---|---|
SyberX is an operating system microkernel used for safety and security-critical applications, such as avionics and unmanned vehicles. In this paper, we present an effective approach to apply formal methods in the development and security evaluation high-assurance level of the SyberX based on Common Criteria (CC) methodology. To achieve the evaluation under the CC at evaluation assurance level 5 augmented (EAL5+), where "+" is applying formal methods compliant to the highest evaluation assurance level, several partners from industry and academia have contributed to this effort. Our work provides a standardized formal specification, security analysis as well as formal verification proofs of the SyberX system. All results have been formalized in the Isabelle/HOL theorem prover. During the verification and code review, we find a total of 5 bugs, all confirmed and fixed by developers. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1007/978-3-030-90870-6_46 | FORMAL METHODS, FM 2021 |
Keywords | DocType | Volume |
Formal methods, High-assurance, SyberX, Common criteria, Isabelle/HOL | Conference | 13047 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
0 | 7 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Wenjing Xu | 1 | 0 | 0.34 |
| Yongwang Zhao | 2 | 0 | 0.68 |
| Chengtao Cao | 3 | 0 | 0.34 |
| Jean Raphael Ngnie Sighom | 4 | 0 | 0.34 |
| Lei Wang | 5 | 5 | 1.96 |
| Zhe Jiang | 6 | 0 | 0.34 |
| Shihong Zou | 7 | 469 | 26.19 |