Amazon Technologies, Inc.

Fortinet, Inc.

Carsten Varming

Neha Rungta

John Byron Cook

Andrew Jude Gacek

Catherine Dodge

Daniel George Peebles

Pauline Virginie Bolignano

Sean McLaughlin

Jeff Puchalski

Juan Rodriguez Hortala

Andrea Nedic

Michael Tautschnig

Mark Rogers Tuttle

Serdar Tasiran

Cole Nathan Schlesinger

Kasper Søe Luckow

Kasper Soe Luckow

Daniel Kroening

Alejandro Naser Pastoriza

Yijou Chen

Rajesh Viswanathan

Theodore M Reed

Sowmya A Karmali

Xiaofei Guo

Temesghen Kahsai Azene

Tyler Stuart Bray

Matti A Vanninen

John Payyappillil John

Nolan K Karpinski

Michael William Whalen

Santosh Kalyankrishnan

Daryl Stephen Cooke

Ian Nicholas Sweet

Zhen Zhang

Nicholas W Mcnutt

Christopher Hall

Andrew Judge Gacek

Murphy Berzish

Daniel Schwartz-Narbonne

An illustrative method includes scanning a compute environment associated with an entity and identifying one or more attack paths from a network to one or more datasets associated with the entity. The one or more attack paths each include a series of risk artifacts within the compute environment that can be exploited by an attacker to access the one or more datasets. The method further includes generating one or more attack path risk scores associated with the one or more attack paths and indicative of one or more levels of risk that the one or more attack paths could be exploited to access the one or more datasets. A risk mitigation operation associated with the one or more attack paths is performed based on the one or more attack path risk scores.

Attack path risk mitigation by a data platform

Methods, systems, and computer-readable media for analysis of role reachability with transitive tags are disclosed. An access control analyzer determines a graph including nodes and edges. The nodes represent roles in a provider network hosting resources. The roles are associated with access control policies granting or denying access to individual resources. One or more of the access control policies grant or deny access based (at least in part) on key-value attributes. The access control analyzer determines, based (at least in part) on a role reachability analysis of the graph, whether a first role can assume a second role using role assumption steps for a particular state of the attributes. The attributes may include transitive attributes that persist during the role assumption steps.

Analysis of role reachability with transitive tags

Methods, systems, and computer-readable media for analysis of role reachability using policy complements are disclosed. An access control analyzer determines two nodes in a graph that potentially have a common edge. The nodes correspond to roles in a provider network, and the roles are associated with first and second access control policies that grant or deny access to resources. The access control analyzer performs a role reachability analysis that determines whether the first role can assume the second role for a particular state of one or more key-value tags. The role reachability analysis determines a third access control policy authorizing a negation of a role assumption request for the second role. The role reachability analysis performs analysis of the third access control policy with respect to a role assumption policy for the second role for the particular state of the one or more key-value tags.

Analysis of role reachability using policy complements

Security policies may be utilized to grant or deny permissions related to the access of computing resources. Two or more security policies may be compared to determine whether the policies are equivalent, whether one security is more permissive than another, and more. In some cases, it may be possible to identify whether there exists a security permission that is sufficient to determine two security policies lack equivalency. Propositional logics may be utilized in the evaluation of security policies.

Security policy analyzer service and satisfiability engine

Techniques are described for generating a specification of security-relevant behavior associated with web services of a cloud provider network. Source code or software development artifacts associated with an implementation of a web service is obtained, where the source code of software development artifacts include an implementation of a request handler for an action of the service. The request handler includes a request authorization component, e.g., which may involve interaction with an identity and access management service of the cloud provider network to authenticate and authorize requests and may further rely upon one or more authorization contexts included in the requests received by the request handler. An interprocedural data flow analyzer is used to analyze a model representation of the bytecode to identify and generate specifications of authorization patterns associated with the request handler.

Analyzing web service frontends to extract security-relevant behavior information

Techniques for intent-based governance are described. For example, in some instances a method of receiving an indication of a change involving of one or more of code, a policy, a network configuration, or a governance requirement rule impacting a resource in a provider network for an account that is to be analyzed using one or more governance requirement rules; determining one or more governance requirement rules to evaluate for compliance after the update; evaluating the determined one or more governance requirement rules for compliance using one or more reasoning engines according to one or more policies; and making a result of the evaluating available to a user provides such governance.

Intent-based governance service

A policy auditing service can be implemented, in accordance with at least one embodiment that obtains a set of parameters that indicates a snapshot of a policy configuration for an account, a query, and a security policy. The security policy may encode a security requirement or invariant. The policy auditing system may determine states that can be reached via mutative operations (e.g., role assumption) and use a policy analyzer service to determine whether assuming a role results in a grant of access that is at least as permissive as the security policy of the set of parameters.

Techniques for analyzing security in computing environments with privilege escalation

Techniques are described for using compositional reasoning techniques to perform role reachability analyses relative to collections of user accounts and roles of a cloud provider network. Delegated role-based resource management generally is a method for controlling access to resources in cloud provider networks and other distributed systems. Many cloud provider networks, for example, implement identity and access management subsystems using this approach, where the concept of 'roles' is used to specify which resources can be accessed by people, software, or (recursively) by other roles. An abstraction of the role reachability analysis is provided that can be used as input to a model-checking application to reason about such role reachability questions (e.g., which roles of an organization are reachable from other roles).

Compositional reasoning techniques for role reachability analyses in identity systems

A method for verifying source code for a program includes determining that a new version of the source code is available. One or more verification tools are determined to use for verification of the new version of the source code from a verification specification associated with the source code. A plurality of verification tasks to perform for the verification of the new version of the source code are automatically determined from the verification specification associated with the source code. The plurality of verification tasks for the new version of the source code are automatically performed using the one or more verification tools. A determination is then made as to whether the new version of the source code is verified.

Automated software verification service

A document anonymization system transforms structured documents, such as security policies, that contain user-specific and other sensitive data, producing encoded logic problems in the format or language of one or more constraint solvers; the logic problems do not contain any of the sensitive data. The system may perform a one- or two-stage anonymization process: in a first stage, the electronic document is analyzed according to its document type to identify parameters likely to contain sensitive data, and the associated values are replaced with arbitrary values; in a second stage, after the anonymized electronic document is converted into logic formulae representing the data, the system performs replacements of string constants in the logic formulae with arbitrary strings to further anonymize the sensitive data. The system may confirm that anonymization preserves the document structure, difficulty level, and satisfiability of the original document by executing the constraint solver against the anonymized logic problem.

Anonymizing sensitive data in logic problems for input to a constraint solver

A security assessment system of a computing resource service provider performs security analyses of virtual resource instances, such as virtual machine instances and virtual data store instances, to verify that certain invariable security requirements are satisfied by the instances' corresponding configurations; these analyses are performed before the instances are provisioned and deployed. If the security checks, which can be selected by the administrator of the resources, fail, the requested resources are denied deployment. Notifications identifying the faulty configuration(s) may be send to the administrative user. A template for launching virtual resource instances may be transformed into an optimized template for performing the pre-deployment security checks, such as by storing information needed to perform the checks within the optimized template itself.

Pre-deployment security analyzer service for virtual computing resources

A constraint solver service of a computing resource service provider performs evaluations of logic problems provided by the service provider's users and/or services by deploying a plurality of constraint solvers to concurrently evaluate the logic problem. Each deployed solver has, or is configured with, different characteristics and/or capabilities than the other solvers; thus, the solvers can have varying execution times and ways of finding a solution. The service may control execution of the solvers using virtual computing resources, such as by installing and configuring a solver to execute in a software container instance. The service receives solver results and delivers them according to a solution strategy such as 'first received' to reduce latency or 'check for agreement' to validate the solution. An interface allows the provider of the logic problem to select and configure solvers, issue commands and modifications during solver execution, select the solution strategy, and receive the solution.

Constraint solver execution service and infrastructure therefor

A security policy analyzer service of a computing resource service provider performs evaluations of security policies provided by the service provider's users, to determine whether the security policies are valid, satisfiable, accurate, and/or sufficiently secure. The service may compare the user-provided policy to a stored or best-practices policy to begin the evaluation, translating encoded security permissions into propositional logic formulae that can be compared to determine which policy is more permissive. The service determines values of the parameters in a request for access to a computing resource based on the policy comparison, and generates request contexts using the values. The service uses the request contexts to generate one or more comparative policies that are then used iteratively as the second policy in the comparison to the user-provided policy, in order to produce additional request contexts that represent allow/deny 'edge cases' along the borders of policy permission statements.

Request context generator for security policy validation service

Growing community of inventors

Brooklyn, NY, United States of America

Carsten Varming