我们专注于提供最先进的专业产品 —— 安全的形式化验证的操作系统内核和用于现代安全产品的Hypervisor。
在这个万物互联的新时代，随着自动驾驶汽车和机器人等行业的蓬勃发展，市场对于高度安全、永不宕机的操作系统有着非常强劲的需求。只有经过形式化验证的操作系统才能达到如此严格的可用性和安全性要求。
操作系统常见问题：
- 典型的未经验证的操作系统内核往往存在安全漏洞，从而导致其不稳定性
- 操作系统一般用C语言编写，容易出现严重的内存漏洞
- 操作系统实现通常没有完整的规范可供遵循
为什么要验证？
实现正确性的形式化的、数学的、机器可检查的证明，确保了该实现完全遵从了其设计规范的语义。
验证的操作系统的设计规范，除了确保其安全运行外，往往还包含内核的机密性、完整性和可用性等经典安全属性。
权能管理模型（Capability-based Access Control），支持对系统中的单个实体访问特定资源进行非常细粒度的管控，通过最小权限原则（POLA）支持强大的安全性。这是高度安全系统的核心设计原则，也是以Linux或Windows为代表的主流系统的访问控制方式无法实现的。
我们的优势
先进的混合关键操作系统
我们的操作系统基于最广泛使用的开源 seL4操作系统微内核，并经过验证。
机器可检查的安全的操作系统
机器可检查的证明确保的实现正确性及规范设计所包含的安全性，确保时间关键系统的安全。
细粒度访问控制
通过功能细粒度访问控制提高安全性。
合规支持
除了 seL4 继承的特性外，我们还支持 MISRA、ASIL-D 和 CC EAL 等合规性以及对 RISC-V 相关硬件的性能调优。
了解更多操作系统产品信息
联系我们
