![]() |
ИСТИНА |
Войти в систему Регистрация |
ФНКЦ РР |
||
The talk presents formal security model of Linux distributions provided by Bazalt SPO, which integrates multi-level security (MLS) and mandatory integrity control (MIC) implemented on the base of SELinux framework. The model also includes information flows analysis framework described as an extended Take-Grant model. The main novelty of the model is the integration of MLS and MIC that can be implemented in SELinux. The model is specified in a hierarchical manner on Event-B language, its security properties are represented as invariants and formally proved.