To transform cybersecurity and privacy research into a highly integrated, community-wide effort, researchers need a common, rich, representative research infrastructure that meets the needs across all members of the research community, and facilitates reproducible science. USC Information Sciences Institute and Northeastern University are meeting researcher needs, and have been funded by the NSF mid-scale research infrastructure program to build Security and Privacy Heterogeneous Environment for Reproducible Experimentation (SPHERE). SPHERE research infrastructure will offer access to an unprecedented variety of user-configurable hardware, software, and network resources, it will offer six user portals geared toward different populations of users, and it will support reproducible research via a combination of infrastructure services and community engagement activities.

With the growing prevalence of cloud computing, providing secure access to information stored in the cloud has become a critical problem. Due to the complexity of access control policies, administrators may inadvertently allow unintended access to private information, and this is a common source of data breaches in cloud based services. In this paper, we present a quantitative symbolic analysis approach for automated policy repair in order to fix overly permissive policies. We encode the semantics of the access control policies using SMT formulas and assess their permissiveness using model counting. Given a policy, a permissiveness bound, and a set of requests that should be allowed, we iteratively repair the policy through permissiveness reduction and refinement, so that the permissiveness bound is reached while the given set of requests are still allowed. We demonstrate the effectiveness of our automated policy repair technique by applying it to policies written in Amazon's AWS Identity and Access Management (IAM) policy language.

Starting with a random initial seed, fuzzers search for inputs that trigger bugs or vulnerabilities. However, fuzzers often fail to generate inputs for program paths guarded by restrictive branch conditions. In this paper, we show that by first identifying rare-paths in programs (i.e., program paths with path constraints that are unlikely to be satisfied by random input generation), and then, generating inputs/seeds that trigger rare-paths, one can improve the coverage of fuzzing tools. In particular, we present techniques 1) that identify rare paths using quantitative symbolic analysis, and 2) generate inputs that can explore these rare paths using path-guided concolic execution. We provide these inputs as initial seed sets to three state of the art fuzzers. Our experimental evaluation on a set of programs shows that the fuzzers achieve better coverage with the rare-path based seed set compared to a random initial seed.

Due to ubiquitous use of software services, protecting the confidentiality of private information stored in compute clouds is becoming an increasingly critical problem. Although access control specification languages and libraries provide mechanisms for protecting confidentiality of information, without verification and validation techniques that can assist developers in writing policies, complex policy specifications are likely to have errors that can lead to unintended and unauthorized access to data, possibly with disastrous consequences. In this paper, we present a quantitative and differential policy analysis framework that not only identifies if one policy is more permissive than another policy, but also quantifies the relative permissiveness of access control policies. We quantify permissiveness of policies using a model counting constraint solver. We present a heuristic that transforms constraints extracted from access control policies and significantly improves the model counting performance. We demonstrate the effectiveness of our approach by applying it to policies written in Amazon's AWS Identity and Access Management (IAM) policy language and Microsoft's Azure policy language.

quacky is a tool for quantifying permissiveness of access control policies in the cloud. Given a policy, quacky translates it into a SMT formula and uses a model counting constraint solver to quantify permissiveness. When given multiple policies, quacky not only determines which policy is more permissive, but also quantifies the relative permissiveness between the policies. With quacky, policy authors can automatically analyze complex policies, helping them ensure that there is no unintended access to private data. quacky supports access control policies written in the Amazon Web Services (AWS) Identity and Access Management (IAM), Microsoft Azure, and Google Cloud Platform (GCP) policy languages. It has command-line and web interfaces. It is open-source and available at https://github.com/vlab-cs-ucsb/quacky.