CPC G06F 21/572 (2013.01) [G06F 9/44589 (2013.01); G06F 21/126 (2013.01); G06F 21/577 (2013.01); G06F 21/629 (2013.01)] | 20 Claims |
1. An embedded system comprising:
a processor operated via a kernel executable by the processor, the kernel being formally proven to satisfy at least one security property;
a hardware peripheral;
a memory; and
an application software program recorded in the memory, the application software program being executed via the formally proven kernel, the application software program being not formally proven or not entirely formally proven, and
wherein the formally proven kernel, executes the application software program, and forces the application software program to execute a policy of controlling access to the hardware peripheral, wherein the formally proven kernel verifies that execution of the application software program does not go against, or complies with, the policy for controlling access to the hardware peripheral,
wherein the formally proven kernel imposes on the application software program the policy for controlling access to the hardware peripheral,
wherein the at least one security property is a policy
for security relative to integrity of data and/or instructions transmitted to and/or from the hardware peripheral,
for privacy of data transmitted to and/or from the hardware peripheral,
for controlling access to the hardware peripheral by the application software program and/or by at least one additional application software program, and/or
for direction of circulation of data and/or instructions transmitted to and/or from the hardware peripheral.
|