The Block Access Controller (BAC) is a mediator between clients of possibly different security levels and any kind of read/write storage (disk, FLASH, DRAM). The interface permits block reads and writes according to the Bell-LaPadula model, where the reads can be from your own level or lower levels, and writes are always to your own level. The BAC can be thought of as behaving like a software “data diode.”
The BAC includes a formal proof of key security and safety properties, in particular that only the intended information flows are possible and that error states are unreachable. The BAC comprises less than 800 lines of C code, which is generated directly from the formal model used to demonstrate these properties. This design simplicity enables cost-effective high assurance solutions.
The main benefits of the BAC are that it has lower Space Weight and Power (SWAP) requirements than a hardware data diode, and more ports. It can be hosted on a MILS operating system, or as a trusted component in a secure virtualization environment. The BAC is the key policy enforcement point for the Trusted Services Engine, and has also been used to stream data between security domains.