Sponsored by: Shape Security

Abstract

Shape Security, a cybersecurity startup, employs a reverse proxy server system named Pegasus to protect their customers' network traffic against attacks. Pegasus is configured by software in a feature-oriented paradigm, composing components of domain-specific code to tailor security policies for customers. Since Shape's composition system has no developer-written way to enforce constraints between components, creating valid compositions is difficult. Our project addresses this issue by enabling a means for predicates to be written for components by the developers. This allows the use of programmable first order logic to validate that all components in a given policy satisfy the features' predicates. The result is a new language which tests facts using logic to validate policies.

Download

• Final report: pdf