CS Seminar Talk - Dr. Kristopher Micinski

Title: Language-Based Security at Scale 

Abstract 

Security and programming languages go hand in hand: precisely defining
and reasoning about a program’s security requires us to reason about
its semantics.  For example, we might define a security policy that
allows the user's location to be revealed, but only after clicking a
particular button to consent. It would seem natural to use techniques
from programming languages (such as static analysis or bug finding) to
automatically check security properties of programs. Unfortunately
this has proven challenging, as reasoning about security properties
often requires scaling these techniques in ways that are
foundationally challenging--e.g., the need for a system model,
inherent path explosion, and tailoring analysis precision to security
relevant program properties.

In this talk, I will outline a vision for scaling language-based
security to the next generation of systems. I will concentrate on two
broad directions. The first is scaling bug finding to uncover
vulnerabilities in production applications. My current work in this
direction uses a novel combination of logs from application runs and
symbolic execution to sidestep the need for an a priori system model
and its attendant path explosion. I will discuss the implementation of
Hogarth, a reverse engineering tool that helps security auditors
understand how the permissions an Android apps uses are triggered via
symbolic execution. The next direction is building efficient compilers
for policy-agnostic programs. Policy-agnostic programming is a
paradigm in which access to secret program data is arbitrated by a
declarative policy (for example, a secret variable "grade" may be
declared as observable only by the instructor). These languages offer
expressive security policies, but often at the expense of runtime
overhead to regulate access to sensitive data. I will discuss a novel
static analysis methodology to verify and optimize policy-agnostic
programs.

Biography

Kristopher Micinski is an assistant professor at Syracuse University,
working at the intersection of programming languages, security, and
systems. His current work is scaling program analyses to production
languages/systems and using those analyses to measure or enhance
security for end users. Kris also collaborates on work in several
related directions, including HCI and formal logics for security.