Object capabilities are a technique for fine-grained
privilege separation in programming languages and systems,
with important applications in security. However, current formal characterisations do not fully capture capability-safety of
a programming language and are not sufficient for verifying
typical applications. Using state-of-the-art techniques from
programming languages research, we define a logical relation
capability-safety. The relation is powerful enough to reason
about typical capability patterns and supports evolvable invariants on shared data structures, capabilities with restricted
authority over them and isolated components with restricted
communication channels. We use a novel notion of effect
parametricity for deriving properties about effects. Our results
imply memory access bounds that have previously been used
to characterise capability-safety.
Secure authentication and authorization within Facebook’s infrastructure play important
roles in protecting people using Facebook’s services. Enforcing security while maintaining a
flexible and performant infrastructure can be challenging at Facebook’s scale, especially in the
presence of varying layers of trust among our servers. Providing authentication and encryption
on a per-connection basis is certainly necessary, but also insufficient for securing more complex
flows involving multiple services or intermediaries at lower levels of trust.
To handle these more complicated scenarios, we have developed two token-based mechanisms
for authentication. The first type is based on certificates and allows for flexible verification due
to its public-key nature. The second type, known as “crypto auth tokens”, is symmetric-key
based, and hence more restrictive, but also much more scalable to a high volume of requests.
Crypto auth tokens rely on pseudorandom functions to generate independently-distributed keys
for distinct identities.
Finally, we provide (mock) examples which illustrate how both of our token primitives can be
used to authenticate real-world flows within our infrastructure, and how a token-based approach
to authentication can be used to handle security more broadly in other infrastructures which
have strict performance requirements and where relying on TLS alone is not enough.
We study some of the concepts, protocols, and algorithms for access control
in distributed systems, from a logical perspective. We account for how a
principal may come to believe that another principal is making a request,
either on his own or on someone else’s behalf. We also provide a logical
language for access control lists, and theories for deciding whether requests
should be granted.
We describe a theory of authentication and a system that implements it. Our theory is based on
the notion of principal and a ‘speaks for’ relation between principals. A simple principal either
has a name or is a communication channel; a compound principal can express an adopted role or
delegated authority. The theory shows how to reason about a principal’s authority by deducing
the other principals that it can speak for; authenticating a channel is one important application.
We use the theory to explain many existing and proposed security mechanisms. In particular, we
describe the system we have built. It passes principals efficiently as arguments or results of remote
procedure calls, and it handles public and shared key encryption, name lookup in a large
name space, groups of principals, program loading, delegation, access control, and revocation.
The ACL model is unable to make correct access decisions for interactions involving more than
two principals, since required information is not retained across message sends. Though this
deficiency has long been documented in the published literature, it is not widely understood. This
logic error in the ACL model is exploited by both the clickjacking and Cross-Site Request
Forgery attacks that affect many Web applications.