Validation is the formal, mathematical, machine-checkable proof of correct implementation of operations to ensure total adherence to the semantics of a design specification.
Aside from secure operation, a kernel based on a fully validated operating system design often includes classic properties such as confidentiality, integrity and availability.
A Capability-based Access Control model supports fine-grain control over access to specific resources by individual entities in the system. Such an access control model achieves strong security through the principle of least privilege (POLA). Such core design principles for highly secure systems are impossible with the current standard access control approach of mainstream systems represented by Linux or Windows.
Advanced Hybrid Critical Operating Systems
Our operating system is based on the most widely used open source seL4 operating system microkernel and is fully validated.
Machine-checkable and Secure Operating System
Machine-checkable proof ensures the correct implementation of security as defined in the design specification and ensures the security of time-critical systems.
Fine-Grain Access Control
Security is vastly improved through fine-grain access control.
In addition to the features inherited from seL4, we support compliance with MISRA, ASIL-D, CC EAL and performance tuning of RISC-V-related hardware.