Visible to the public A High-Assurance Partitioned Development Environment