A Methodology For Micro-Policies
This thesis proposes a formal methodology for defining, specifying, and reasoning about micro-policies — security policies based on fine-grained tagging that include forms of access control, memory safety, compartmentalization, and information-flow control. Our methodology is based on a symbolic mac...
Main Author: | |
---|---|
Format: | Text |
Language: | English |
Published: |
ScholarlyCommons
2017
|
Subjects: | |
Online Access: | https://repository.upenn.edu/edissertations/2881 https://repository.upenn.edu/cgi/viewcontent.cgi?article=4667&context=edissertations |
id |
ftunivpenn:oai:repository.upenn.edu:edissertations-4667 |
---|---|
record_format |
openpolar |
spelling |
ftunivpenn:oai:repository.upenn.edu:edissertations-4667 2023-05-15T18:32:43+02:00 A Methodology For Micro-Policies Azevedo De Amorim, Arthur 2017-01-01T08:00:00Z application/pdf https://repository.upenn.edu/edissertations/2881 https://repository.upenn.edu/cgi/viewcontent.cgi?article=4667&context=edissertations en eng ScholarlyCommons https://repository.upenn.edu/edissertations/2881 https://repository.upenn.edu/cgi/viewcontent.cgi?article=4667&context=edissertations Publicly Accessible Penn Dissertations Computer Security Formal Verification Memory Safety Reference Monitors Computer Sciences text 2017 ftunivpenn 2021-01-04T22:03:29Z This thesis proposes a formal methodology for defining, specifying, and reasoning about micro-policies — security policies based on fine-grained tagging that include forms of access control, memory safety, compartmentalization, and information-flow control. Our methodology is based on a symbolic machine that extends a conventional RISC-like architecture with tags. Tags express security properties of parts of the program state ("this is an instruction," "this is secret," etc.), and are checked and propagated on every instruction according to flexible user-supplied rules. We apply this methodology to two widely studied policies, information-flow control and heap memory safety, implementing them with the symbolic machine and formally characterizing their security guarantees: for information-flow control, we prove a classic notion of termination-insensitive noninterference; for memory safety, a novel property that protects memory regions that a program cannot validly reach through the pointers it possesses — which, we believe, provides a useful criterion for evaluating and comparing different flavors of memory safety. We show how the symbolic machine can be realized with a more practical processor design, where a software monitor takes advantage of a hardware cache to speed up its execution while protecting itself from potentially malicious user-level code. Our development has been formalized and verified in the Coq proof assistant, attesting that our methodology can provide rigorous security guarantees. Text The Pointers University of Pennsylvania: ScholaryCommons@Penn |
institution |
Open Polar |
collection |
University of Pennsylvania: ScholaryCommons@Penn |
op_collection_id |
ftunivpenn |
language |
English |
topic |
Computer Security Formal Verification Memory Safety Reference Monitors Computer Sciences |
spellingShingle |
Computer Security Formal Verification Memory Safety Reference Monitors Computer Sciences Azevedo De Amorim, Arthur A Methodology For Micro-Policies |
topic_facet |
Computer Security Formal Verification Memory Safety Reference Monitors Computer Sciences |
description |
This thesis proposes a formal methodology for defining, specifying, and reasoning about micro-policies — security policies based on fine-grained tagging that include forms of access control, memory safety, compartmentalization, and information-flow control. Our methodology is based on a symbolic machine that extends a conventional RISC-like architecture with tags. Tags express security properties of parts of the program state ("this is an instruction," "this is secret," etc.), and are checked and propagated on every instruction according to flexible user-supplied rules. We apply this methodology to two widely studied policies, information-flow control and heap memory safety, implementing them with the symbolic machine and formally characterizing their security guarantees: for information-flow control, we prove a classic notion of termination-insensitive noninterference; for memory safety, a novel property that protects memory regions that a program cannot validly reach through the pointers it possesses — which, we believe, provides a useful criterion for evaluating and comparing different flavors of memory safety. We show how the symbolic machine can be realized with a more practical processor design, where a software monitor takes advantage of a hardware cache to speed up its execution while protecting itself from potentially malicious user-level code. Our development has been formalized and verified in the Coq proof assistant, attesting that our methodology can provide rigorous security guarantees. |
format |
Text |
author |
Azevedo De Amorim, Arthur |
author_facet |
Azevedo De Amorim, Arthur |
author_sort |
Azevedo De Amorim, Arthur |
title |
A Methodology For Micro-Policies |
title_short |
A Methodology For Micro-Policies |
title_full |
A Methodology For Micro-Policies |
title_fullStr |
A Methodology For Micro-Policies |
title_full_unstemmed |
A Methodology For Micro-Policies |
title_sort |
methodology for micro-policies |
publisher |
ScholarlyCommons |
publishDate |
2017 |
url |
https://repository.upenn.edu/edissertations/2881 https://repository.upenn.edu/cgi/viewcontent.cgi?article=4667&context=edissertations |
genre |
The Pointers |
genre_facet |
The Pointers |
op_source |
Publicly Accessible Penn Dissertations |
op_relation |
https://repository.upenn.edu/edissertations/2881 https://repository.upenn.edu/cgi/viewcontent.cgi?article=4667&context=edissertations |
_version_ |
1766216907451531264 |