NDLI: Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security

Content Provider	ACM Digital Library
Author	Hardekopf, Ben Chong, Frederic T. Oberg, Jason K. Li, Xun Levin, Timothy Valamehr, Jonathan Kastner, Ryan Tiwari, Mohit Sherwood, Timothy
Abstract	High assurance systems used in avionics, medical implants, and cryptographic devices often rely on a small trusted base of hardware and software to manage the rest of the system. Crafting the core of such a system in a way that achieves flexibility, security, and performance requires a careful balancing act. Simple static primitives with hard partitions of space and time are easier to analyze formally, but strict approaches to the problem at the hardware level have been extremely restrictive, failing to allow even the simplest of dynamic behaviors to be expressed. Our approach to this problem is to construct a minimal but configurable architectural skeleton. This skeleton couples a critical slice of the low level hardware implementation with a microkernel in a way that allows information flow properties of the entire construction to be statically verified all the way down to its gate-level implementation. This strict structure is then made usable by a runtime system that delivers more traditional services (e.g. communication interfaces and long-living contexts) in a way that is decoupled from the information flow properties of the skeleton. To test the viability of this approach we design, test, and statically verify the information-flow security of a hardware/software system complete with support for unbounded operation, inter-process communication, pipelined operation, and I/O with traditional devices. The resulting system is provably sound even when adversaries are allowed to execute arbitrary code on the machine, yet is flexible enough to allow caching, pipelining, and other common case optimizations.
Starting Page	189
Ending Page	200
Page Count	12
File Format	PDF MP4
ISSN	01635964
DOI	10.1145/2024723.2000087
Journal	ACM SIGARCH Computer Architecture News (CARN)
Volume Number	39
Issue Number	3
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1981-04-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Non-interference Gate level information flow tracking High assurance systems
Content Type	Audio Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security

Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security

Crafting a usable microkernel, processor, and i/o system with strict and provable information flow security.

Gate-Level Information Flow Tracking for Security Lattices

Expanding Gate Level Information Flow Tracking for Multilevel Security

An Improved Encoding Technique for Gate Level Information Flow Tracking

Generating optimized gate level information flow tracking logic for enforcing multilevel security

Execution leases: a hardware-supported mechanism for enforcing strong non-interference

High-assurance systems such as those found in ind...

Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security

Similar Documents

Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security

Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security

Crafting a usable microkernel, processor, and i/o system with strict and provable information flow security.

Gate-Level Information Flow Tracking for Security Lattices

Expanding Gate Level Information Flow Tracking for Multilevel Security

An Improved Encoding Technique for Gate Level Information Flow Tracking

Generating optimized gate level information flow tracking logic for enforcing multilevel security

Execution leases: a hardware-supported mechanism for enforcing strong non-interference

High-assurance systems such as those found in ind...

Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security