東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Designing Information Flow Secure Ha...

Li, Xun.

Linked to FindBook

Google Book

Amazon

博客來

Designing Information Flow Secure Hardware.

Record Type:	Language materials, printed : Monograph/item
Title/Author:	Designing Information Flow Secure Hardware./
Author:	Li, Xun.
Description:	180 p.
Notes:	Source: Dissertation Abstracts International, Volume: 75-01(E), Section: B.
Contained By:	Dissertation Abstracts International75-01B(E).
Subject:	Computer Science. -
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3596184
ISBN:	9781303426131

Designing Information Flow Secure Hardware.
Li, Xun.

Designing Information Flow Secure Hardware. - 180 p.

Source: Dissertation Abstracts International, Volume: 75-01(E), Section: B.

Thesis (Ph.D.)--University of California, Santa Barbara, 2013.

Systems that require strong guarantees on security policies such as those used in banking and military rely on the proper implementation of the underlying hardware in respect to the flow of information. The most challenging task has been to design such systems with provable security properties without generating significant overhead. We show that it is possible and practical to design provably information flow secure embedded processors with minimum hardware overhead. Our insight is that programming language techniques for secure information flow can be applied to the field of hardware design to enable the creation of synchronous hardware designs that are statically-verifiable as secure. Such static techniques, when used in combination with dynamic information flow tracking, can achieve significant reduction in hardware overhead and increase in expressiveness.

ISBN: 9781303426131Subjects--Topical Terms:

626642
Computer Science.

Designing Information Flow Secure Hardware.
LDR:03299nam a2200277 4500 001 1960605
005 20140623111239.5
008 150210s2013 ||||||||||||||||| ||eng d
020 $a 9781303426131
035 $a (MiAaPQ)AAI3596184
035 $a AAI3596184
040 $a MiAaPQ $c MiAaPQ
100 1 $a Li, Xun. $3 723417
245 1 0 $a Designing Information Flow Secure Hardware.
300 $a 180 p.
500 $a Source: Dissertation Abstracts International, Volume: 75-01(E), Section: B.
500 $a Adviser: Frederic T. Chong.
502 $a Thesis (Ph.D.)--University of California, Santa Barbara, 2013.
520 $a Systems that require strong guarantees on security policies such as those used in banking and military rely on the proper implementation of the underlying hardware in respect to the flow of information. The most challenging task has been to design such systems with provable security properties without generating significant overhead. We show that it is possible and practical to design provably information flow secure embedded processors with minimum hardware overhead. Our insight is that programming language techniques for secure information flow can be applied to the field of hardware design to enable the creation of synchronous hardware designs that are statically-verifiable as secure. Such static techniques, when used in combination with dynamic information flow tracking, can achieve significant reduction in hardware overhead and increase in expressiveness.
520 $a This dissertation presents an exploration of various approaches in designing hardware with strong security guarantees. We start by introducing Execution Lease, an architectural enforcement mechanism built upon a completely dynamic information flow tracking infrastructure. The idea is to associate every bit of data with security tags and maintain them precisely at runtime. These information are then used to provide timing and space boundary when invoking untrusted program components. In order to be able to formally reason about security properties of the resulting hardware, we propose Caisson, a programming language extension of Verilog that allows designers to specify security policies through a security type system along with explicit state machined based model. To maintain the capability of static verification while completely eliminating the need of duplicating resource for different security levels, we combine dynamic tracking techniques with language-based static verification, and introduce a new programming language Sapper. Sapper also allows designers to specify security types for data and signals, which instead of being type checked, will physically exist after fabrication and serve for the purpose of dynamic tracking. Runtime tracking and enforcement logic is generated by static analysis on the language such that the hardware overhead can be minimized along with static guarantees. At the end, we use Sapper to build complex embedded processor that is guaranteed to enforce non-interference, and we show that the hardware overhead is minimum.
590 $a School code: 0035.
650 4 $a Computer Science. $3 626642
690 $a 0984
710 2 $a University of California, Santa Barbara. $b Computer Science. $3 1018455
773 0 $t Dissertation Abstracts International $g 75-01B(E).
790 $a 0035
791 $a Ph.D.
792 $a 2013
793 $a English
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3596184