This talk focuses on verification of information flow security for a simple separation kernel and briefly on synthesis of a protector to enforce information flow policies in Java Programs A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information security for a simple separation kernel for ARMv7. Limiting the kernel functionality as much as meaningfully possible, we accomplish a detailed analysis and verification of the system, proving its correctness at the level of the ARMv7 assembly. The verification is done in HOL4 taking the Cambridge model of ARM as basis transferring verification tasks on the actual assembly code to an adaptation of the BAP binary analysis tool developed at CMU We also present a method for synthesising a symbolic prediction-based. monitor that observes a program at certain checkpoints, predicts confidentiality violations, and applies suitable countermeasures to prevent information leakage. We prove the soundness of our method and implement a tool-set that automates the whole process and generates a self-protecting layer for Java application using AspectJ.
مستنداتی یافت نشد.