Curriculum Vitae

(A link to the PDF version is here.)

Andrew K. Hirsch

http://www.cs.cornell.edu/~akhirsch

akhirsch@cs.cornell.edu

Education

Research Interests

Theses and Research Projects

Authorization logics are often used to describe correctness for authorizaiton mechanisms in distributed systems. They allow flexibility in defining authorization policies and proof-theoretic tools for providing security guarantees. However, these logics generally do not reflect the fact that often authorization decisions are based on private or low-integrity data. We (Hirsch, Cecchetti, Arden, and Tate) are developing FLAFOL, the Flow-Limited Authorization First-Order Logic, which is an authorization logic with information flow labels. FLAFOL describes the correctness of authorization mechanisms which respect information flow policies. FLAFOL also provides unique security guarantees: not only do the standard notions of non-interference for authorization logic and information flow labels hold, but we can show that the action of a correct authorization mechanism (with reference to FLAFOL) cannot leak private information, as determined by the labels.

Effects are ubiquitous in programming languages. Ever since Moggi introduced monads in his computational lambda calculus, there have been generalizations and reformulations of categorical semantics of effect systems. My work involves pushing back on the assumptions that are made in these models, and in applying those models to understand issues in programming languages. My most recent work involves relaxing the assumptions about the structure of the language that these models are built on.

Authorization logics are used to describe and prove properties of authorization policies. We give a new semantics for authorization logics, based on the informal notion of semantics for the Nexus Authorization Logic (NAL). We show that this semantics is equivalent to the more traditional Kripke semantics. This work was published in Computer and Communications Security 2013 in Berlin, Germany.

Composite is a component-based operating system developed at The George Washington University. I developed a domain specific language for specifing communication between components. The language automatically inserted dynamic checks to ensure that communication happened correctly. This served as my Capstone Design project for my Bachelor’s of Science degree.

Turing categories are a definition of computability in category theory. I discuss Turing categories, and note their use in proving theories in computability theory. This served as an Honor’s thesis for my Bachelor’s of Science degree.

Teaching Experience

Part-Time Graduate Teaching Assistant, Cornell University

Graduate Teaching Assistant, Cornell University

Graduate Teaching Assistant, Cornell University

Graduate Teaching Assistant, Cornell University

Graduate Teaching Assistant, Cornell University

Undergraduate Teaching Assistant, The George Washington University

Undergraduate Teaching Assistant, The George Washington University

Past Positions

Writing and Talks

Service

Selected Relevant Courses