SNoAnd.github.io/index.html at main · SNoAnd/SNoAnd.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
<head>
<style>
.collapsible {
  background-color: #777;
  color: white;
  cursor: pointer;
  padding: 18px;
  width: 100%;
  border: none;
  text-align: left;
  outline: none;
  font-size: 15px;
}

.active, .collapsible:hover {
  background-color: #555;
}

.content {
  padding: 0 18px;
  display: none;
  overflow: hidden;
  background-color: #f1f1f1;
}
</style>
<link rel="shortcut icon" type="image/png" href="favicon.png">
</head>
<body>
<title>Sean Noble Anderson</title>

<table>
<tr>
<td>
<IMG SRC="headshot.jpg" ALIGN=top ALT="(PHOTO)" STYLE="width:128px">
</td>
<td>
<h1>Sean Noble Anderson</h1>
<h2>PhD Candidate<BR>
<a href="http://www.cs.pdx.edu">Department of Computer Science</a><BR>
<a href="http://www.pdx.edu">Portland State University</a><BR>
</h2>
<h4>
B.S., Computer Science, <a href="http://www.cs.clarkson.edu">Clarkson University</a>, 2013.
<br>
</h4>

<a href="mailto:ander28@pdx.edu">ander28@pdx.edu</a> -
<a href="mailto:sean.noble.anderson@protonmail.com">sean.noble.anderson@protonmail.com</a>
<br>
<a href="resume.pdf">Download resume</a> -
<a href="">LinkedIn</a> -
<a href="">Github</a>
</tr>
</table>

<h2>About me</h2>

I'm a PhD candidate researching formal methods, verification, programming languages,
and logic. I am currently particularly focused in applying these techniques to security:
making software safer with math!
My present work is on protecting C code using novel hardware-level tagging
mechanisms to perform security monitoring. This work is
<a href="https://nsf.gov/awardsearch/showAward?AWD_ID=2048499">graciously supported<a/>
by the NSF.
<hr>

<a name="proj"><h3> Projects </h3></a>

<h4>Tagged C</h4>

<p>
<a href="https://github.com/SNoAnd/Tagged-C">Tagged C</a> is a C variant with a flexible, built-in security monitor supporting a range of different security policies.
</p>

<button type="button" class="collapsible">Read more about Tagged C</button>
<div class="content">

Tag-based reference monitoring is a model of dynamic security enforcement in which every
piece of data in a system is paired with an associatted piece of metadata, called a tag.
Tags carry information related to the role or history of data: concepts like
"this string is from user input," "this pointer gives write access to object X,"
"this value carries Bob's personal information." A monitor, implemented in software or hardware,
can read the tags on data involved in the current step, update tags on any computational results,
and issue an interrupt if the system would take a step with a bad combination of tags---say,
printing Bob's personal information to a public channel.

Tagged C is a C variant with a reference monitor built in, enabling the user to provide
a policy definition and have it enforced during execution.

The current technical contributions of the project consist of the formal semantics (based on
that of CompCert) and a reference interpreter, implemented in coq and extracted to ocaml.
The interpreter is proven to replicate the behavior of the semantics.

Going forward, I'm working on proving safety properties of compartmentalization policies,
while my labmate Allison Naaktgebooren is building a harness to use Tagged C with specialized policies
to fuzz-test programs.

<p>
<a href="rv23.pdf">
	"Flexible Runtime Security Enforcement with Tagged C"
</a>
(joint with Allison Naaktgeboren and <a href="https://www.cecs.pdx.edu/~apt/">Andrew Tolmach</a>),
<i>RV 23</i>, October 2023.
</p>
<p>
<a href="https://dl.acm.org/doi/pdf/10.1145/3437992.3439929">
	"Towards Formally Verified Compilation of Tag-Based Policy Enforcement"
</a>
(joint with CHR Chhak and <a href="https://www.cecs.pdx.edu/~apt/">Andrew Tolmach</a>),
<i>CPP 2021</i>, January 2021.
</p>
</div>

<h4>Formally Defining Stack Safety</h4>

<p>
In this line of theoretical work, I've attempted to tease out the essence of what it means to call a system "stack safe" and capture that essence in a <a href="https://github.com/SNoAnd/stack-safety">testable definition</a>.
</p>
<button type="button" class="collapsible">Read more about stack safety</button>
<div class="content">

There are so many different mechanisms out there that purport to protect the call stack
from attack, from extremely light-weight ones like stack canaries to sophisticated memory
protection. My group originally set out to test one (the tag-based PIPE policies of
<a href="https://ic.ese.upenn.edu/pdf/stack_ieeesp2018.pdf">Roessler and DeHon</a>,
but quickly found that it was not at all obvious what we should be testing!
It turns out that stack safety is quite finicky to describe formally.

I was particularly interested in the question of "lazy" enforcement, a style of policy
described by Roessler and DeHon that allows unsafe writes, but prevents them from being
read, for performance reasons. Focusing on this rather strange edge-case helped guide
us toward the observation that stack safety is about the flow of information between
caller and callee.

<p>
<a href="csf23.pdf">"Formalizing Stack Safety as a Security Property"</a> (joint with
<a href="https://robblanco.github.io/">Roberto Blanco</a>,
<a href="https://lemonidas.github.io">Leonidas Lamproploulos</a>,
<a href="https://www.cis.upenn.edu/~bcpierce/">Benjamin C. Pierce</a>, and
<a href="https://web.cecs.pdx.edu/~apt/">Andrew Tolmach</a>),
<i>CSF 2023</i>, July 2023.
</p>

</div>

<a name="pubs"><h3> Other Publications</h3></a>

<p>
"Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor" (joint with
  Zhenyang Dai,
  Shuang Liu,
  Vilhelm Sjoberg,
  Xupeng Li,
  Yu Chen,
  Wenhao Wang,
  Yuekai Jia,
  Laila Elbeheiry,
  Shubham Sondhi,
  Yu Zhang,
  Zhaozhong Ni,
  Shoumeng Yan,
  Ronghui Gu, and
  Zhengyu He),
  <i>ASPLOS 2024</i>, April 2024.
</p>
<hr>

<h3>Personal Links</h3>

<script>
var coll = document.getElementsByClassName("collapsible");
var i;

for (i = 0; i < coll.length; i++) {
  coll[i].addEventListener("click", function() {
    this.classList.toggle("active");
    var content = this.nextElementSibling;
    if (content.style.display === "block") {
      content.style.display = "none";
    } else {
      content.style.display = "block";
    }
  });
}
</script>

</body>