NDLI: Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis

Please wait, while we are loading the content...

Big Data Analytics and Intelligence at Alibaba Cloud

Determining Application-specific Peak Power and Energy Requirements for Ultra-low Power Processors

REDSPY: Exploring Value Locality in Software

Failure-Atomic Slotted Paging for Persistent Memory

ProRace: Practical Data Race Detection for Production Use

Black-box Concurrent Data Structures for NUMA Architectures

Optimizing CNNs on Multicores for Scalability, Performance and Goodput

Improving Datacenter Efficiency

DudeTM: Building Durable Transactions with Decoupling for Persistent Memory

Graspan: A Single-machine Disk-based Graph System for Interprocedural Static Analyses of Large-scale Systems Code

Efficient Address Translation for Architectures with Multiple Page Sizes

FLEP: Enabling Flexible and Efficient Preemption on GPUs

Identifying Security Critical Properties for the Dynamic Verification of a Processor

Bolt: I Know What You Did Last Summer... In The Cloud

Automated Synthesis of Comprehensive Memory Model Litmus Test Suites

Hardware-Software Co-design to Mitigate DRAM Refresh Overheads: A Case for Refresh-Aware Process Scheduling

Enabling Lightweight Transactions with Precision Time

Prophet: Precise QoS Prediction on Non-Preemptive Accelerators to Improve Utilization in Warehouse-Scale Computers

Translation-Triggered Prefetching

What Scalable Programs Need from Transactional Memory

Crossing Guard: Mediating Host-Accelerator Coherence Interactions

CoRAL: Confined Recovery in Distributed Asynchronous Graph Processing

Locality Transformations for Nested Recursive Iteration Spaces

ReFlex: Remote Flash ≈ Local Flash

SC-DCNN: Highly-Scalable Deep Convolutional Neural Network using Stochastic Computing

Page Fault Support for Network Controllers

SaberLDA: Sparsity-Aware Learning of Topic Models on GPUs

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis

Neurosurgeon: Collaborative Intelligence Between the Cloud and Mobile Edge

DCatch: Automatically Detecting Distributed Concurrency Bugs in Cloud Systems

Kill the Program Counter: Reconstructing Program Behavior in the Processor Cache Hierarchy

IncBricks: Toward In-Network Computation with an In-Network Cache

Mallacc: Accelerating Memory Allocation

Typed Architectures: Architectural Support for Lightweight Scripting

TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA

An Architecture Supporting Formal and Compositional Binary Analysis

KickStarter: Fast and Accurate Computations on Streaming Graphs via Trimmed Approximations

Locality-Aware CTA Clustering for Modern GPUs

Approximate Storage of Compressed and Encrypted Videos

3DGates: An Instruction-Level Energy Analysis and Optimization of 3D Printers

Towards "Full Containerization" in Containerized Network Function Virtualization

Moonwalk: NRE Optimization in ASIC Clouds

CHERI JNI: Sinking the Java Security Model into the C

Thermostat: Application-transparent Page Management for Two-tiered Main Memory

Towards Practical Default-On Multi-Core Record/Replay

TETRIS: Scalable and Efficient Neural Network Acceleration with 3D Memory

AMNESIAC: Amnesic Automatic Computer

An Analysis of Persistent Memory Use with WHISPER

AsyncClock: Scalable Inference of Asynchronous Event Causality

Browsix: Bridging the Gap Between Unix and the Browser

Sound Loop Superoptimization for Google Native Client

Exploiting Intra-Request Slack to Improve SSD Performance

Dynamic Resource Management for Efficient Utilization of Multitasking GPUs

GRIFFIN: Guarding Control Flows Using Intel Processor Trace

Breaking the Boundaries in Heterogeneous-ISA Datacenters

Pallas: Semantic-Aware Checking for Finding Deep Bugs in Fast Path

History-Based Arbitration for Fairness in Processor-Interconnect of NUMA Servers

Voltage Regulator Efficiency Aware Power Management

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis

Content Provider	ACM Digital Library
Author	Suh, G. Edward Zhang, Danfeng Ferraiuolo, Andrew Myers, Andrew C. Xu, Rui
Abstract	Hardware-based mechanisms for software isolation are becoming increasingly popular, but implementing these mechanisms correctly has proved difficult, undermining the root of security. This work introduces an effective way to formally verify important properties of such hardware security mechanisms. In our approach, hardware is developed using a lightweight security-typed hardware description language (HDL) that performs static information flow analysis. We show the practicality of our approach by implementing and verifying a simplified but realistic multi-core prototype of the ARM TrustZone architecture. To make the security-typed HDL expressive enough to verify a realistic processor, we develop new type system features. Our experiments suggest that information flow analysis is efficient, and programmer effort is modest. We also show that information flow constraints are an effective way to detect hardware vulnerabilities, including several found in commercial processors.
Starting Page	555
Ending Page	568
Page Count	14
File Format	PDF
ISBN	9781450344654
DOI	10.1145/3037697.3037739
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2017-04-04
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Hardware security Information flow Trustzone
Content Type	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

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis (CARN, Vol. 45, Issue. 1)

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis (OPSR, Vol. 51, Issue. 2)

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis (SIGP, Vol. 52, Issue. 4)

Collaborative Verification of Information Flow for a High-Assurance App Store

Lightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis (Technical Report)

Static information flow analysis for java.

Static information flow analysis for Java (2008)

A Design and Verification Methodology for a TrustZone Trusted Execution Environment

Secure information flow analysis for hardware design: using the right abstraction for the job

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis

Similar Documents

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis (CARN, Vol. 45, Issue. 1)

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis (OPSR, Vol. 51, Issue. 2)

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis (SIGP, Vol. 52, Issue. 4)

Collaborative Verification of Information Flow for a High-Assurance App Store

Lightweight Verification of Secure Hardware Isolation Through Static Information Flow Analysis (Technical Report)

Static information flow analysis for java.

Static information flow analysis for Java (2008)

A Design and Verification Methodology for a TrustZone Trusted Execution Environment

Secure information flow analysis for hardware design: using the right abstraction for the job

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis