As cloud computing gains widespread adoption across various industries, securing cloud resources has become a top priority for cloud providers. However, ensuring configuration security among highly interconnected cloud resources is challenging due to the complexities of resource modeling, correlation analysis, and large-scale security checks. To tackle those practical challenges, we propose Security Invariants (SI), a precise, effective, and scalable tool that proactively protects cloud resources by automated security reasoning. We have integrated SI into the rigorous Amazon Web Services (AWS) security review process. Partnered with security engineers and other security scanners, SI periodically scans billions of cloud resources in pre-launch services for potential security risks, maximizing the security guarantees of cloud applications. The continuous assessment of evolving resources not only brings a deep understanding of cloud security risks but also introduces a generalized solution from the holistic security analysis perspective.

Abstract Over the past ten years, the adoption of cloud services has grown rapidly, leading to the introduction of automated deployment tools to address the scale and complexity of the infrastructure companies and users deploy. Without the aid of automation, ensuring the security of an ever-increasing number of deployments becomes more and more challenging. To the best of our knowledge, no formal automated technique currently exists to verify cloud deployments during the design phase. In this case study, we show that Description Logic modeling and inference capabilities can be used to improve the safety of cloud configurations. We focus on the Amazon Web Services (AWS) proprietary declarative language, CloudFormation, and develop a tool to encode template files into logic. We query the resulting models with properties related to security posture and report on our findings. By extending the models with dataflow-specific knowledge, we use more comprehensive semantic reasoning to further support security reviews. When applying the developed toolchain to publicly available deployment files, we find numerous violations of widely-recognized security best practices, which suggests that streamlining the methodologies developed for this case study would be beneficial.

Cloud computing provides on-demand access to IT resources via the Internet. Permissions for these resources are defined by expressive access control policies. This paper presents a formalization of the Amazon Web Services (AWS) policy language and a corresponding analysis tool, called ZELKOVA, for verifying policy properties. ZELKOVA encodes the semantics of policies into SMT, compares behaviors, and verifies properties. It provides users a sound mechanism to detect misconfigurations of their policies. ZELKOVA solves a PSPACE-complete problem and is invoked many millions of times daily.

Current dynamic analysis tools for Android applications do not get good code coverage since they can only explore a subset of the behaviors of the applications and do not have full control over the environment in which they execute. In this work we use model checking to systematically explore application paths while reducing the analysis size using state matching and backtracking. In particular, we extend the Java PathFinder (JPF) model checking environment for Android. We describe the difficulties one needs to overcome to make this a reality as well as our current approaches to handling these issues. We obtain significantly higher coverage using shorter event sequences on a representative sample of Android apps, when compared to Dynodroid and Sapienz, the current state-of-the-art dynamic analysis tools for Android applications.

Verification of Graphical User Interface (GUI) applications presents many challenges. GUI applications are open systems that are driven by user events. Verification of such applications by means of model checking therefore requires a user model in order to close the state space. In addition, GUIs rely extensively on complex and inherently concurrent framework libraries such as AWT/Swing, for which the application code merely provides callbacks. Software model checking of GUI applications therefore needs abstractions of such frameworks that faithfully preserve application behavior. This paper presents JPF-AWT, an extension of the Java PathFinder software model checker, which addresses these challenges. JPF-AWT has been successfully applied to a GUI front end of a NASA ground data system.

To be effective, software model checking needs powerful reduction techniques. In this paper, we present an experimental study that demonstrates effectiveness of environment generation combined with slicing as a model generation and reduction technique. Automatic environments were obtained using the Bandera Environment Generator (BEG) and slicing was performed using the Indus Java slicer. The results show that environment generation implemented in BEG is an aggressive reduction technique. However, it may miss behaviors in the environment and consequently in the module under analysis, making it unsafe. As such, this technique can be effective for detection of errors but not sufficient to prove their absence.Slicing, while a safe technique, may be too approximate and not scalable. Also, slicing implemented in Indus requires a closed system and cannot be safely applied to a module without its environment. In this paper, we show how environment generation and slicing can be combined to detect errors and prove their absence. We applied the combined approach to verify parts of Fujitsu's enterprise software called Interstage Business Process Management (I-BPM)

Model checking can be an effective technique for detecting concurrency-related errors in software systems. However, due to scalability issues, to handle industrial-strength software, model checking needs to be combined with powerful reduction techniques. In this work, we applied modular model checking to detect errors in Interstage Business Process Management (I-BPM) software, a Java client-server application spanning more than 500,000 lines of code. To model check a separate module, one needs to represent its context of execution, i.e., its environment. Environment generation is a significant challenge, since the environment is to be general enough to uncover the module's errors, yet restrictive enough to allow tractable model checking.In this paper, we present an experimental study that demonstrates the effectiveness of environment generation as a reduction technique in general and the effectiveness of automated environment generation in particular. Since model checking of the original application was intractable, we compared performance of automatically generated environments to environments written previously by hand. Automatic environments were obtained using Bandera Environment Generator (BEG). We present results of modular verification for both manual and automatic environments. The results show that automatically generated environments produce systems with a smaller state space, yet, for faulty modules, uncover the errors and, for error-free modules, produce coverage similar to manual environments.

A key problem in model checking open systems is environment modeling (i.e., representing the behavior of the execution context of the system under analysis). Software systems are fundamentally open since their behavior is dependent on patterns of invocation of system components and values defined outside the system but referenced within the system. Whether reasoning about the behavior of whole programs or about program components, an abstract model of the environment can be essential in enabling sufficiently precise yet tractable verification. In this paper, we describe an approach to generating environments of Java program fragments. This approach integrated formally specified assumptions about environment behavior with sound abstractions of environment implementations to form a model of the environment. The approach is implemented in the Bandera environment generator (BEG) which we describe along with our experience using BEG to reason about properties of several nontrivial concurrent Java programs.

There is a widely held belief that whole program analysis is intractable for large complex software systems, and there can be little doubt that this is true for program analyses based on model checking. Model checking selected program components that comprise a cohesive unit, however, can be an effective way of uncovering subtle coding errors, especially for components of multi-threaded programs. In this setting, one of the chief problems is how to safely approximate the behavior of the rest of the application as it relates to the unit being analyzed.Non-unit application components are collectively referred to as the environment. In this paper, we describe how points-to and side-effects analyses can be adapted to support generation of summaries of environment behavior that can be reified into Java code using special modeling primitives. The resulting abstract models of the environment can be combined with the code of the unit and then model checked against unit properties. We present our analysis framework, illustrate its flexibility in generating several types of models, and present experience that provides evidence of the scalability of the approach.