Timing Covert Channel Analysis of the VxWorks MILS Embedded Hypervisor under the Common Criteria Security Certification

TL;DR

This paper introduces a new experimental method to analyze timing covert channels in embedded hypervisors, demonstrated through a case study on VxWorks MILS, highlighting potential security vulnerabilities and aiding system robustness assessments.

Contribution

It presents a novel approach for assessing timing covert channels in embedded hypervisors, applied to a commercial product for security certification.

Findings

Timing covert channels can be established in VxWorks MILS hypervisor

The approach helps evaluate system robustness against information leakage

Assists in security certification processes

Abstract

Virtualization technology is nowadays adopted in security-critical embedded systems to achieve higher performance and more design flexibility. However, it also comes with new security threats, where attackers leverage timing covert channels to exfiltrate sensitive information from a partition using a trojan. This paper presents a novel approach for the experimental assessment of timing covert channels in embedded hypervisors, with a case study on security assessment of a commercial hypervisor product (Wind River VxWorks MILS), in cooperation with a licensed laboratory for the Common Criteria security certification. Our experimental analysis shows that it is indeed possible to establish a timing covert channel, and that the approach is useful for system designers for assessing that their configuration is robust against this kind of information leakage.