Notice of Pre-AIA or AIA Status
The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA .
This office action is in response to claims filed 03/30/2023. Claims 1-20 are pending.
Claim Objections
Claims 5, 13, and 16 are objected to because of the following informalities:
Regarding Claim 5, lines 5-6 state “the second SMT solver system obtains results from two or more of the plurality of the plurality of SMT solvers.” This should state “the second SMT solver system obtains results from two or more of the plurality of SMT solvers” instead, and is being interpreted as such for examination.
Regarding Claim 13, line 2 states “storing, by the first SMT solver system, first metrics related a first execution time.” This should state “storing, by the first SMT solver system, first metrics related to a first execution time” instead, and is being interpreted as such for examination.
Regarding Claim 16, lines 5-6 state “the second SMT solver system obtains results from two or more of the plurality of the plurality of SMT solvers.” This should state “the second SMT solver system obtains results from two or more of the plurality of SMT solvers” instead, and is being interpreted as such for examination.
Appropriate correction is required.
Claim Rejections - 35 USC § 103
The following is a quotation of 35 U.S.C. 103 which forms the basis for all obviousness rejections set forth in this Office action:
A patent for a claimed invention may not be obtained, notwithstanding that the claimed invention is not identically disclosed as set forth in section 102, if the differences between the claimed invention and the prior art are such that the claimed invention as a whole would have been obvious before the effective filing date of the claimed invention to a person having ordinary skill in the art to which the claimed invention pertains. Patentability shall not be negated by the manner in which the invention was made.
Claims 1-20 are rejected under 35 U.S.C. 103 as being unpatentable over Jain (US 20220292210 A1) in view of Huston, III et al. (US 20210367979 A1), hereinafter referred to as Jain and Huston, respectively.
Regarding Claim 1, Jain discloses A computer-implemented method ([0031] a computer processor of a machine learning privilege assignment platform may receive an indication of a user vector for a user from a user vector generator. Please note the process carried out by a computer processor corresponds to Applicant’s computer-implemented method.) comprising:
receiving, by an automated reasoning service of a cloud provider network, a request identifying: a policy managed by an identity and access management service of the cloud provider network, and a property expressing a desired condition of the policy ([0022] The system 100 functions may be performed by a constellation of networked apparatuses, such as in a distributed processing or cloud-based architecture.; [0027] The machine learning privilege assignment platform 330 might use the accessed information, for example, to help determine a privilege decision based on a user vector and a change requested by a user (e.g., a decision granting or denying access to the user). The process might be performed automatically; [0031] a computer processor of a machine learning privilege assignment platform may receive an indication of a user vector for a user from a user vector generator. The machine learning privilege assignment platform might, for example, need to generate a privilege decision based on a requested computing environment change being made by that user. Please note that the cloud system with a machine learning privilege assignment platform that receives a requested computing environment change corresponds to Applicant’s automated reasoning service of a cloud provider network that receives a request identifying a policy managed by an identity and access management service of the cloud provider network and a property expressing a desired condition of the policy, as the requested change and determination of privilege decision further correspond to the policy and property expressing a desired condition.);
invoking a first SMT solver system based on the policy and the property, wherein the first SMT solver system includes a modeler and a plurality of SMT solvers ([0032] The SMT solver may, for example, review the privilege decision before granting the user access to the computing environment. Note that the SMT solver may act as a global policy check.; [0047] When the context is determined, the system runs an SMT solver against the policy. The SMT solver checks to determine if the policies defined for the resource violate any global policy checks.; [0049] This vector representation can then be used to train a model based on data (e.g., having a neural network learn a function) as to whether a specific devop should be allowed to modify a config or not. Please note that the SMT solver reviewing the privilege decision before granting the user access as a global policy check, where models are further trained after the SMT solvers’ operation corresponds to Applicant’s invoking a first SMT solver system based on the policy and the property, wherein the first SMT solver system includes a modeler and a plurality of SMT solvers), wherein invoking the first SMT solver system causes the first SMT solver system to:
generate, by the modeler, a first-order logic formula based on the policy and the property, and provide the first-order logic formula to the plurality of SMT solvers to obtain first results data indicating whether the first-order logic formula is satisfiable or unsatisfiable ([0034] As used herein, the term “SMT solver” may be associated with a formula in first-order logic and/or whether such a formula is satisfiable.; [0049] This vector representation can then be used to train a model based on data (e.g., having a neural network learn a function) as to whether a specific devop should be allowed to modify a config or not. This is where context may be captured from historical data. Please note that the first-order logic formula that is to be associated with the SMT solver as well as whether it is satisfiable corresponds to Applicant’s modeler generating a first-order logic formula based on the policy and the property and providing it to the plurality of SMT solvers to obtain first results data indicating whether it is satisfiable. );
Jain does not explicitly disclose invoking a second SMT solver system based on the policy, the property, and the first results data;
obtaining second results data from the second SMT solver system;
and causing display of data indicating whether first results data differs from the second results data.
However, Huston discloses invoking a second SMT solver system based on the policy, the property, and the first results data ([0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that using one or more SMT operations to reduce the dimensionality of the security policy corresponds to Applicant’s invoking a second SMT solver system, i.e., another SMT operation distinct from a first, based on the policy, the property, and the first results data as previously recited by Jain.);
obtaining second results data from the second SMT solver system ( [0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that the results of the second SMT operation corresponds to Applicant’s obtaining second results data from the second SMT solver system.);
and causing display of data indicating whether first results data differs from the second results data ([0004] two or more security policies are presented with visual indicia representing differences between the security policies; [0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that the visual presentation using results of the SMT operations, where security policies may be presented with visual indicia representing differences between the security policies, corresponds to Applicant’s causing display of data indicating whether first results data differs from the second results data, as it would be obvious to a person of ordinary skill in the art to display multiple results and compare them using the UI.).
Jain and Huston are both considered to be analogous to the claimed invention because they are in the same field of utilizing SMT for the implementation of security/access control in computer networks. Therefore, it would have been obvious to someone of ordinary skill in the art prior to the effective filing date of the claimed invention to have modified Jain to incorporate the teachings of Huston to modify the system receiving a request to modify a policy and a property and invoking a first SMT solver system with a first-order logic formula based on the policy and the property in order to obtain first results data to invoke a second SMT solver based on the policy, property, and first results data, obtaining second results, and displaying the data indicating whether the two results data differ, allowing for improved analysis and enforcement of security policies, as described in Huston.
Regarding Claim 2, Jain-Huston as described in Claim 1, Jain further discloses invoking the first SMT solver system further causes the first SMT solver system to: obtain the first results data based on an earliest result received from an SMT solver of the plurality of SMT solvers, and terminate SMT solvers of the plurality of SMT solvers from which the earliest result was not obtained ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. […] the system access decision and/or other information maybe fed back to the devop vector generator 610 and/or machine learning privilege assignment platform 630 (as illustrated by dashed lines in FIG. 6) to further train or otherwise tune the performance of the system. Please note that past results being used to improve performance of the system through feedback data corresponds to Applicant’s first SMT solver system obtaining the first results data based on an earliest result received from an SMT solver of the plurality of SMT solvers, as the system performance in future executions, i.e., when invoking the first SMT solver system to obtain the first results data, may be influenced by past results data, i.e., an earliest result received from an SMT solver of the plurality of SMT solvers. Furthermore, since the feedback data is from past results that may improve performance, i.e., from the execution of specific SMT solvers that performed better than others, this corresponds to terminating SMT solvers of the plurality of SMT solvers from which the earliest result was not obtained. These previous SMT solvers would have already completed processing, i.e., been terminated, and in an instance in which subsequent SMT solver executions after the earliest one did not improve performance, they would be terminated while not containing the earliest result.);
and wherein the second SMT solver system obtains results from two or more of the plurality of SMT solvers, and wherein the second results data includes the results from two or more of the plurality of SMT solvers ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. […] the system access decision and/or other information maybe fed back to the devop vector generator 610 and/or machine learning privilege assignment platform 630 (as illustrated by dashed lines in FIG. 6) to further train or otherwise tune the performance of the system. Please note that past results being used to improve performance of the system through feedback data corresponds to Applicant’s second SMT solver system obtaining results from two or more of the plurality of SMT solvers, and wherein the second results data includes the results from two or more of the plurality of SMT solvers, as the system performance in future executions, i.e., when running the second SMT solver system, may be influenced by past results data, i.e., may obtain results from multiple of the plurality of results data from SMT solvers stored as part of the feedback data. As the feedback data may include results data from two or more of the plurality of SMT solvers that have completed operations, this corresponds to Applicant’s second results data including the results for two or more SMT solvers.).
Regarding Claim 3, Jain-Huston as described in Claim 1, Jain further discloses the second SMT solver system differs from the first SMT solver system based on at least one of: a different implementation of the modeler, or one or more different configurations of the modeler ([0036] an SMT solver may check the policy during design time. This can be deployed as a service and checks may be made for each config (because the configuration tends to change). Please note that the configuration changing and being checked by the SMT solver during design time corresponds to Applicant’s second SMT solver system differing from the first based on different configurations of the modeler. As Applicant states “one or more of” the differences, this is interpreted as fulfilling the requirement.).
Regarding Claim 4, Jain discloses A computer-implemented method ([0031] a computer processor of a machine learning privilege assignment platform may receive an indication of a user vector for a user from a user vector generator. Please note the process carried out by a computer processor corresponds to Applicant’s computer-implemented method.) comprising:
receiving a request identifying a policy associated with one or more computing resources and a property expressing a desired condition of the policy ([0022] The system 100 functions may be performed by a constellation of networked apparatuses, such as in a distributed processing or cloud-based architecture.; [0027] The machine learning privilege assignment platform 330 might use the accessed information, for example, to help determine a privilege decision based on a user vector and a change requested by a user (e.g., a decision granting or denying access to the user). The process might be performed automatically; [0031] a computer processor of a machine learning privilege assignment platform may receive an indication of a user vector for a user from a user vector generator. The machine learning privilege assignment platform might, for example, need to generate a privilege decision based on a requested computing environment change being made by that user. Please note that the cloud system with a machine learning privilege assignment platform that receives a requested computing environment change corresponds to Applicant’s receiving a request identifying a policy associated with computing resources and a property expressing a desired condition of the policy, as the requested change and determination of privilege decision further correspond to the policy and property expressing a desired condition.);
invoking a first SMT solver system based on the policy and the property ([0032] The SMT solver may, for example, review the privilege decision before granting the user access to the computing environment. Note that the SMT solver may act as a global policy check.; [0047] When the context is determined, the system runs an SMT solver against the policy. The SMT solver checks to determine if the policies defined for the resource violate any global policy checks.; [0049] This vector representation can then be used to train a model based on data (e.g., having a neural network learn a function) as to whether a specific devop should be allowed to modify a config or not. Please note that the SMT solver reviewing the privilege decision before granting the user access as a global policy check, where models are further trained after the SMT solvers’ operation corresponds to Applicant’s invoking a first SMT solver system based on the policy and the property.), wherein the first SMT solver system:
generates a formula based on the policy and the property, and provides the formula to a plurality of SMT solvers to obtain first results data indicating whether the formula is satisfiable or unsatisfiable ([0034] As used herein, the term “SMT solver” may be associated with a formula in first-order logic and/or whether such a formula is satisfiable.; [0049] This vector representation can then be used to train a model based on data (e.g., having a neural network learn a function) as to whether a specific devop should be allowed to modify a config or not. This is where context may be captured from historical data. Please note that the first-order logic formula that is to be associated with the SMT solver as well as whether it is satisfiable corresponds to Applicant’s modeler generating a formula based on the policy and the property and providing it to the plurality of SMT solvers to obtain first results data indicating whether it is satisfiable. );
Jain does not explicitly disclose invoking a second SMT solver system based on the policy, the property, and the first result data;
obtaining second results data from the second SMT solver system;
and providing data indicating whether the first results data differs from the second results data to another component.
However, Huston discloses invoking a second SMT solver system based on the policy, the property, and the first result data ([0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that using one or more SMT operations to reduce the dimensionality of the security policy corresponds to Applicant’s invoking a second SMT solver system, i.e., another SMT operation distinct from a first, based on the policy, the property, and the first results data as previously recited by Jain.);
obtaining second results data from the second SMT solver system ( [0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that the results of the second SMT operation corresponds to Applicant’s obtaining second results data from the second SMT solver system.);
and providing data indicating whether the first results data differs from the second results data to another component ([0004] two or more security policies are presented with visual indicia representing differences between the security policies; [0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that the visual presentation using results of the SMT operations, where security policies may be presented with visual indicia representing differences between the security policies, corresponds to Applicant’s providing data indicating whether first results data differs from the second results data, as it would be obvious to a person of ordinary skill in the art to provide multiple results to the display, i.e., another component, and compare them using the UI.).
Jain and Huston are both considered to be analogous to the claimed invention because they are in the same field of utilizing SMT for the implementation of security/access control in computer networks. Therefore, it would have been obvious to someone of ordinary skill in the art prior to the effective filing date of the claimed invention to have modified Jain to incorporate the teachings of Huston to modify the system receiving a request to modify a policy and a property and invoking a first SMT solver system with a formula based on the policy and the property in order to obtain first results data to invoke a second SMT solver based on the policy, property, and first results data, obtaining second results, and provide the data indicating whether the two results data differ, allowing for improved analysis and enforcement of security policies, as described in Huston.
Regarding Claim 5, Jain-Huston as described in Claim 4, Jain further discloses invoking the first SMT solver system further causes the first SMT solver system to: obtain the first results data based on an earliest result received from an SMT solver of the plurality of SMT solvers, and terminate SMT solvers of the plurality of SMT solvers from which the earliest result was not obtained ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. […] the system access decision and/or other information maybe fed back to the devop vector generator 610 and/or machine learning privilege assignment platform 630 (as illustrated by dashed lines in FIG. 6) to further train or otherwise tune the performance of the system. Please note that past results being used to improve performance of the system through feedback data corresponds to Applicant’s first SMT solver system obtaining the first results data based on an earliest result received from an SMT solver of the plurality of SMT solvers, as the system performance in future executions, i.e., when invoking the first SMT solver system to obtain the first results data, may be influenced by past results data, i.e., an earliest result received from an SMT solver of the plurality of SMT solvers. Furthermore, since the feedback data is from past results that may improve performance, i.e., from the execution of specific SMT solvers that performed better than others, this corresponds to terminating SMT solvers of the plurality of SMT solvers from which the earliest result was not obtained. These previous SMT solvers would have already completed processing, i.e., been terminated, and in an instance in which subsequent SMT solver executions after the earliest one did not improve performance, they would be terminated while not containing the earliest result.);
and wherein the second SMT solver system obtains results from two or more of the plurality of the plurality of SMT solvers, and wherein the second results data includes the results from two or more of the plurality of SMT solvers ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. […] the system access decision and/or other information maybe fed back to the devop vector generator 610 and/or machine learning privilege assignment platform 630 (as illustrated by dashed lines in FIG. 6) to further train or otherwise tune the performance of the system. Please note that past results being used to improve performance of the system through feedback data corresponds to Applicant’s second SMT solver system obtaining results from two or more of the plurality of SMT solvers, and wherein the second results data includes the results from two or more of the plurality of SMT solvers, as the system performance in future executions, i.e., when running the second SMT solver system, may be influenced by past results data, i.e., may obtain results from multiple of the plurality of results data from SMT solvers stored as part of the feedback data. As the feedback data may include results data from two or more of the plurality of SMT solvers that have completed operations, this corresponds to Applicant’s second results data including the results for two or more SMT solvers.).
Regarding Claim 6, Jain-Huston as described in Claim 4, Jain further discloses the second SMT solver system differs from the first SMT solver system based on at least one of: a different implementation of a modeler used to generate the formula based on the policy and the property, or one or more different configurations of the modeler ([0036] an SMT solver may check the policy during design time. This can be deployed as a service and checks may be made for each config (because the configuration tends to change). Please note that the configuration changing and being checked by the SMT solver during design time corresponds to Applicant’s second SMT solver system differing from the first based on different configurations of the modeler. As Applicant states “one or more of” the differences, this is interpreted as fulfilling the requirement.).
Regarding Claim 7, Jain-Huston as described in Claim 4, Jain further discloses storing, by the first SMT solver system, the first results data in a storage resource accessible to the first SMT solver system and the second SMT solver system ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. Please note that the feedback data that is being used as past results to improve performance of the system must necessarily be stored in a storage resource, as is known in the art, such that it is accessible in the future, i.e., accessible by the second SMT solver system. Therefore, this corresponds to Applicant’s first SMT solver system storing first results data in a storage resource accessible to the first and second SMT solver systems. );
and obtaining, by the second SMT solver system, the first results data from the storage resource ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. […] the system access decision and/or other information maybe fed back to the devop vector generator 610 and/or machine learning privilege assignment platform 630 (as illustrated by dashed lines in FIG. 6) to further train or otherwise tune the performance of the system. Please note that feedback data from past privilege results being used to further train the performance of the system corresponds to Applicant’s second SMT solver system obtaining the first results data from the storage resource, i.e., past results data as feedback.).
Regarding Claim 8, Jain-Huston as described in Claim 4, Jain further discloses storing, by the first SMT solver system, a plurality of results data including the first results data in a storage resource accessible to the first SMT solver system and the second SMT solver system ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. Please note that the feedback data that is being used as past results to improve performance of the system must necessarily be stored in a storage resource, as is known in the art, such that it is accessible in the future, i.e., accessible by the second SMT solver system. Therefore, this corresponds to Applicant’s first SMT solver system storing a plurality of results data in a storage resource accessible to the first and second SMT solver systems. );
and wherein the second SMT solver system is invoked on a sampled subset of the plurality of results data stored in the storage resource ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. […] the system access decision and/or other information maybe fed back to the devop vector generator 610 and/or machine learning privilege assignment platform 630 (as illustrated by dashed lines in FIG. 6) to further train or otherwise tune the performance of the system. Please note that past results being used to improve performance of the system through feedback data corresponds to Applicant’s second SMT solver system being invoked on a sampled subset of the plurality of results data stored in the storage resource, as the system performance in future executions, i.e., when running the second SMT solver system, may be influenced by past results data, i.e., a sampled subset of the plurality of results data stored as part of the feedback data corresponding to the storage resource.).
Regarding Claim 9, Jain-Huston as described in Claim 4, Huston further discloses the second SMT solver system includes a second plurality of SMT solvers that is different from the first plurality of SMT solvers, and wherein the second plurality of SMT solvers is different from the first plurality of SMT solvers based on at least one of: the second plurality of SMT solvers includes an additional SMT solver compared to the first plurality of SMT solvers, the second plurality of SMT solvers includes fewer solvers compared to the first plurality of SMT solvers, or the second plurality of SMT solvers includes a different version of a solver in the first plurality of SMT solvers ([0016] Certain embodiments of the disclosed system use advances in formal logic software, such as Satisfiability Modulo Theory solvers (e.g., Z3 solver) to perform analysis of a security policy and present the administrator with a simplified view of the policy effects in an understandable manner at a user interface.; [0024] Z3 is an SMT Solver available from Microsoft Research that may be used to implement certain embodiments of the disclosed system. Please note that SMT solvers, with one example being a Z3 solver available from Microsoft Research, correspond to Applicant’s second SMT solver system including a second plurality of SMT solvers different from the first plurality of SMT solvers based on a different version of a solver in the first plurality of SMT solvers. This is because, as would be able to be recognized by a person of ordinary skill in the art, Z3 solvers being one variant of a solver implies other types, i.e., different versions, of solvers that may be implemented and be different between the first set of SMT solvers and the second. As Applicant states “at least one of” the ways the second plurality may be different, this is interpreted as fulfilling the requirements of the claim.).
Regarding Claim 10, Jain-Huston as described in Claim 4, Huston further discloses invoking a third SMT solver system based on the policy, the property, and the first result data ([0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that using one or more SMT operations to reduce the dimensionality of the security policy corresponds to Applicant’s invoking a third SMT solver system, i.e., another SMT operation distinct from a first and second, based on the policy, the property, and the first results data as previously recited by Jain.);
obtaining third results data from the third SMT solver system ( [0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that the results of the third SMT operation corresponds to Applicant’s obtaining third results data from the third SMT solver system.);
Huston further discloses comparing the third results data to the second results data; and causing display of information indicating a difference between the third results data and the second results data ([0004] two or more security policies are presented with visual indicia representing differences between the security policies; [0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that the visual presentation using results of the SMT operations, where security policies may be presented with visual indicia representing differences between the security policies, corresponds to Applicant’s causing display of information indicating differences between the third and second results data, as it would be obvious to a person of ordinary skill in the art to display multiple results and compare them using the UI.).
Regarding Claim 11, Jain-Huston as described in Claim 4, Huston further discloses generating an alert indicating the difference between the first results data and the second results data ([0004] two or more security policies are presented with visual indicia representing differences between the security policies; [0005] generating a visual presentation on a user interface using results of the SMT operations. Please note that the visual presentation using results of the SMT operations, where security policies may be presented with visual indicia representing differences between the security policies, corresponds to Applicant’s generating an alert indicating the differences between the first and second results data, as it would be obvious to a person of ordinary skill in the art to present an alert to the user as part of the visual presentation on a UI to show the differences between the results data.).
Regarding Claim 12, Jain-Huston as described in Claim 4, Jain further discloses receiving input identifying a plurality of requests, wherein each of the plurality of requests identifies a respective policy and a respective condition; and invoking the second SMT solver system on each request of the plurality of requests ([0027] The machine learning privilege assignment platform 330 might use the accessed information, for example, to help determine a privilege decision based on a user vector and a change requested by a user (e.g., a decision granting or denying access to the user). The process might be performed automatically or be initiated via a command from a remote operator interface device; [0032] The SMT solver may, for example, review the privilege decision before granting the user access to the computing environment. Note that the SMT solver may act as a global policy check. Even, for example, when the neural network indicates that a user should be allowed to make a particular change, if a global policy prohibits that type of change by that type of user it still might not be allowed by the solver. Please note that the machine learning privilege assignment platform reviewing privilege decisions via a SMT solver to process changes requested by users corresponds to Applicant’s receiving input identifying a plurality of requests, with each request identifying a respective policy and condition, and invoking the second SMT solver system on each request. This is because processing multiple requests via the platform and SMT solver would be obvious to do to one of ordinary skill in the art.).
Regarding Claim 13, Jain-Huston as described in Claim 4, Jain further discloses storing, by the first SMT solver system, first metrics related a first execution time of the first SMT solver system to obtain the first results data ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. Please note that the feedback data that is being used as past results to improve performance of the system must necessarily be stored in a storage resource, as is known in the art, such that it is accessible in the future. Furthermore, it is obvious to one of ordinary skill in the art that the results data being used to improve performance of the system may include first metrics related to a first execution time of the first SMT solver system to obtain the first results data, as execution time is a metric known in the art to indicate performance of a computer operation, and would be obvious to be included along with the results and feedback data.);
and storing, by the second SMT solver system, second metrics related to a second execution time of the second SMT solver system to obtain the second results data ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. Please note that the feedback data that is being used as past results to improve performance of the system must necessarily be stored in a storage resource, as is known in the art, such that it is accessible in the future. Furthermore, it is obvious to one of ordinary skill in the art that the results data being used to improve performance of the system may include second metrics related to a second execution time of the second SMT solver system to obtain the second results data, as execution time is a metric known in the art to indicate performance of a computer operation, and would be obvious to be included along with the results and feedback data.).
Regarding Claim 14, Jain-Huston as described in Claim 4, Huston further discloses the results data includes information identifying a version of the first SMT solver system and state information related to the first SMT solver system during invocation of the first SMT solver system ([0016] Satisfiability Modulo Theory solvers (e.g., Z3 solver) to perform analysis of a security policy and present the administrator with a simplified view of the policy effects in an understandable manner at a user interface. The administrator can use the presentation at the user interface to understand an existing policy and, in certain embodiments, to understand the impact of any policy changes. Please note that the SMT solver analyzing a security policy and presenting the policy effects at a UI, where the SMT solver is identified with a version, i.e., being a Z3 solver, and state information, i.e., the policy effects included as part of the resulting output, corresponds to Applicant’s results data including this information related to the first SMT solver system during its invocation.).
Regarding Claim 15, Jain discloses A system comprising: a first one or more electronic devices to implement an automated reasoning service in a multi-tenant provider network ([0022] The system 100 functions may be performed by a constellation of networked apparatuses, such as in a distributed processing or cloud-based architecture.; [0027] The machine learning privilege assignment platform 330 Please note that the system performing functions via a constellation of networked apparatuses, including a machine learning privilege assignment platform, corresponds to Applicant’s system comprising a first electronic devices to implement an automated reasoning service in a multi-tenant provider network), wherein the automated reasoning service includes instructions that upon execution cause the automated reasoning service to ([0024] a computer-readable storage medium may store thereon instructions that when executed by a machine result in performance according to any of the embodiments described herein. Please note that the instructions executed by a machine resulting in performance of the embodiments corresponds to Applicant’s automated reasoning service including instructions that upon execution cause the automated reasoning service to carry out operations.):
receive a request identifying: a policy managed by an identity and access management service of the multi-tenant provider network, and a property expressing a desired condition of the policy ([0022] The system 100 functions may be performed by a constellation of networked apparatuses, such as in a distributed processing or cloud-based architecture.; [0027] The machine learning privilege assignment platform 330 might use the accessed information, for example, to help determine a privilege decision based on a user vector and a change requested by a user (e.g., a decision granting or denying access to the user). The process might be performed automatically; [0031] a computer processor of a machine learning privilege assignment platform may receive an indication of a user vector for a user from a user vector generator. The machine learning privilege assignment platform might, for example, need to generate a privilege decision based on a requested computing environment change being made by that user. Please note that the cloud system with a machine learning privilege assignment platform that receives a requested computing environment change corresponds to Applicant’s receiving a request identifying a policy managed by an identity and access management service of the multi-tenant provider network and a property expressing a desired condition of the policy, as the requested change and determination of privilege decision further correspond to the policy and property expressing a desired condition.);
invoke a first SMT solver system based on the policy and the property, wherein the first SMT solver system includes a modeler and a plurality of SMT solvers to obtain first results data ([0032] The SMT solver may, for example, review the privilege decision before granting the user access to the computing environment. Note that the SMT solver may act as a global policy check.; [0047] When the context is determined, the system runs an SMT solver against the policy. The SMT solver checks to determine if the policies defined for the resource violate any global policy checks.; [0049] This vector representation can then be used to train a model based on data (e.g., having a neural network learn a function) as to whether a specific devop should be allowed to modify a config or not. Please note that the SMT solver reviewing the privilege decision before granting the user access as a global policy check, where models are further trained after the SMT solvers’ operation corresponds to Applicant’s invoking a first SMT solver system based on the policy and the property, wherein the first SMT solver system includes a modeler and a plurality of SMT solvers to obtain results data.);
and a second one or more electronic devices to implement the first SMT solver system in the multi-tenant provider network, wherein the first SMT solver system includes instructions that upon execution cause the first SMT solver system to: generate, by the modeler, a first-order logic formula based on the policy and the property, and provide the first-order logic formula to the plurality of SMT solvers to obtain first results data indicating whether the first-order logic formula is satisfiable or unsatisfiable ([0034] As used herein, the term “SMT solver” may be associated with a formula in first-order logic and/or whether such a formula is satisfiable.; [0049] This vector representation can then be used to train a model based on data (e.g., having a neural network learn a function) as to whether a specific devop should be allowed to modify a config or not. This is where context may be captured from historical data. Please note that the first-order logic formula that is to be associated with the SMT solver as well as whether it is satisfiable corresponds to Applicant’s modeler generating a first-order logic formula based on the policy and the property and providing it to the plurality of SMT solvers to obtain first results data indicating whether it is satisfiable. Furthermore, as the multi-tenant provider network may comprise multiple devices and has instructions for execution of the functions including the SMT solver system, this corresponds to Applicant’s second electronic device to implement the first SMT solver system in the multi-tenant provider network and the first SMT solver system includes instructions that perform the functions when executed.).
Jain does not explicitly disclose invoke a second SMT solver system based on the policy, the property, and the first results data;
obtain second results data from the second SMT solver system;
and causing display of data indicating whether first results data differs from the second results data;
However, Huston discloses invoke a second SMT solver system based on the policy, the property, and the first results data ([0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that using one or more SMT operations to reduce the dimensionality of the security policy corresponds to Applicant’s invoking a second SMT solver system, i.e., another SMT operation distinct from a first, based on the policy, the property, and the first results data as previously recited by Jain.);
obtain second results data from the second SMT solver system ( [0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that the results of the second SMT operation corresponds to Applicant’s obtaining second results data from the second SMT solver system.);
and causing display of data indicating whether first results data differs from the second results data ([0004] two or more security policies are presented with visual indicia representing differences between the security policies; [0005] retrieving a set of rules of a security policy; analyzing the set of rules of the security policy using one or more Satisfiability Modulo Theory (SMT) operations to reduce a dimensionality of the security policy; and generating a visual presentation on a user interface using results of the SMT operations. Please note that the visual presentation using results of the SMT operations, where security policies may be presented with visual indicia representing differences between the security policies, corresponds to Applicant’s causing display of data indicating whether first results data differs from the second results data, as it would be obvious to a person of ordinary skill in the art to display multiple results and compare them using the UI.);
Jain and Huston are both considered to be analogous to the claimed invention because they are in the same field of utilizing SMT for the implementation of security/access control in computer networks. Therefore, it would have been obvious to someone of ordinary skill in the art prior to the effective filing date of the claimed invention to have modified Jain to incorporate the teachings of Huston to modify the system receiving a request to modify a policy and a property and invoking a first SMT solver system with a first-order logic formula based on the policy and the property in order to obtain first results data to invoke a second SMT solver based on the policy, property, and first results data, obtaining second results, and displaying the data indicating whether the two results data differ, allowing for improved analysis and enforcement of security policies, as described in Huston.
Regarding Claim 16, Jain-Huston as described in Claim 15, Jain further discloses invoking the first SMT solver system further causes the first SMT solver system to: obtain the first results data based on an earliest result received from an SMT solver of the plurality of SMT solvers, and terminate SMT solvers of the plurality of SMT solvers from which the earliest result was not obtained ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. […] the system access decision and/or other information maybe fed back to the devop vector generator 610 and/or machine learning privilege assignment platform 630 (as illustrated by dashed lines in FIG. 6) to further train or otherwise tune the performance of the system. Please note that past results being used to improve performance of the system through feedback data corresponds to Applicant’s first SMT solver system obtaining the first results data based on an earliest result received from an SMT solver of the plurality of SMT solvers, as the system performance in future executions, i.e., when invoking the first SMT solver system to obtain the first results data, may be influenced by past results data, i.e., an earliest result received from an SMT solver of the plurality of SMT solvers. Furthermore, since the feedback data is from past results that may improve performance, i.e., from the execution of specific SMT solvers that performed better than others, this corresponds to terminating SMT solvers of the plurality of SMT solvers from which the earliest result was not obtained. These previous SMT solvers would have already completed processing, i.e., been terminated, and in an instance in which subsequent SMT solver executions after the earliest one did not improve performance, they would be terminated while not containing the earliest result.);
and wherein the second SMT solver system obtains results from two or more of the plurality of the plurality of SMT solvers, and wherein the second results data includes the results from two or more of the plurality of SMT solvers ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. […] the system access decision and/or other information maybe fed back to the devop vector generator 610 and/or machine learning privilege assignment platform 630 (as illustrated by dashed lines in FIG. 6) to further train or otherwise tune the performance of the system. Please note that past results being used to improve performance of the system through feedback data corresponds to Applicant’s second SMT solver system obtaining results from two or more of the plurality of SMT solvers, and wherein the second results data includes the results from two or more of the plurality of SMT solvers, as the system performance in future executions, i.e., when running the second SMT solver system, may be influenced by past results data, i.e., may obtain results from multiple of the plurality of results data from SMT solvers stored as part of the feedback data. As the feedback data may include results data from two or more of the plurality of SMT solvers that have completed operations, this corresponds to Applicant’s second results data including the results for two or more SMT solvers.).
Regarding Claim 17, Jain-Huston as described in Claim 15, Jain further discloses the second SMT solver system differs from the first SMT solver system based on at least one of: a different implementation of the modeler, or one or more different configurations of the modeler ([0036] an SMT solver may check the policy during design time. This can be deployed as a service and checks may be made for each config (because the configuration tends to change). Please note that the configuration changing and being checked by the SMT solver during design time corresponds to Applicant’s second SMT solver system differing from the first based on different configurations of the modeler. As Applicant states “one or more of” the differences, this is interpreted as fulfilling the requirement.).
Regarding Claim 18, Jain-Huston as described in Claim 15, Jain further discloses store, by the first SMT solver system, the first results data in a queue provided by a service of a cloud provider network ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. Please note that the feedback data that is being used as past results to improve performance of the system must necessarily be stored in a storage resource, as is known in the art, such that it is accessible in the future, i.e., accessible by the second SMT solver system, wherein the system is operating in a cloud network. Therefore, this corresponds to Applicant’s first SMT solver system storing a plurality of results data in a queue provided by a cloud provider network, as it is known in the art to one of ordinary skill that a queue is a common data storage structure, and would be particularly applicable in this case to be conducive to retrieval of feedback data.);
and obtain, by the second SMT solver system, the first results data from the queue ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. Please note that the feedback data that is being used as past results to improve performance of the system and being accessed by the second SMT solver system corresponds to Applicant’s obtaining the first results data from the queue, as it is known in the art to one of ordinary skill that a queue is a common data storage structure, and would be particularly applicable in this case to be conducive to retrieval of feedback data by the subsequently operating SMT solver, allowing it to operate with improved performance.).
Regarding Claim 19, Jain-Huston as described in Claim 15, Jain further discloses store, by the first SMT solver system, a plurality of results data including the first results data in a storage resource provided by a cloud provider network ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. Please note that the feedback data that is being used as past results to improve performance of the system must necessarily be stored in a storage resource, as is known in the art, such that it is accessible in the future, i.e., accessible by the second SMT solver system, wherein the system is operating in a cloud network. Therefore, this corresponds to Applicant’s first SMT solver system storing a plurality of results data in a storage resource provided by a cloud provider network. );
and wherein the second SMT solver system is invoked on a sampled subset of the plurality of results data ([0035] According to some embodiments, information [..] past privilege decisions and results, etc. may be used to improve performance of the system. For example, FIG. 6 illustrates 600 the use of feedback data according to some embodiments. […] the system access decision and/or other information maybe fed back to the devop vector generator 610 and/or machine learning privilege assignment platform 630 (as illustrated by dashed lines in FIG. 6) to further train or otherwise tune the performance of the system. Please note that past results being used to improve performance of the system through feedback data corresponds to Applicant’s second SMT solver system being invoked on a sampled subset of the plurality of results data stored in the storage resource, as the system performance in future executions, i.e., when running the second SMT solver system, may be influenced by past results data, i.e., a sampled subset of the plurality of results data stored as part of the feedback data corresponding to the storage resource.).
Regarding Claim 20, Jain-Huston as described in Claim 15, Huston further discloses the second SMT solver system includes a second plurality of SMT solvers that is different from the first plurality of SMT solvers ([0016] Certain embodiments of the disclosed system use advances in formal logic software, such as Satisfiability Modulo Theory solvers (e.g., Z3 solver) to perform analysis of a security policy and present the administrator with a simplified view of the policy effects in an understandable manner at a user interface.; [0024] Z3 is an SMT Solver available from Microsoft Research that may be used to implement certain embodiments of the disclosed system. Please note that SMT solvers, with one example being a Z3 solver available from Microsoft Research, correspond to Applicant’s second SMT solver system including a second plurality of SMT solvers different from the first plurality of SMT solvers. This is because, as would be able to be recognized by a person of ordinary skill in the art, Z3 solvers being one variant of a solver implies other types of solvers that may be implemented and be different between the first set of SMT solvers and the second.).
Conclusion
The prior art made of record and not relied upon is considered pertinent to applicant's disclosure.
Chittimalli et al. (US 20200387497 A1) discloses SMT operating on business rules to detect inconsistencies, study the effect of addition of a new policy, determining satisfiability of formulas, and different variants of SMT solvers (see [0002-0003, 0105])
Any inquiry concerning this communication or earlier communications from the examiner should be directed to FARAZ T AKBARI whose telephone number is (571)272-4166. The examiner can normally be reached Monday-Thursday 9:30am-7:30pm ET.
Examiner interviews are available via telephone, in-person, and video conferencing using a USPTO supplied web-based collaboration tool. To schedule an interview, applicant is encouraged to use the USPTO Automated Interview Request (AIR) at http://www.uspto.gov/interviewpractice.
If attempts to reach the examiner by telephone are unsuccessful, the examiner’s supervisor, April Blair can be reached at (571)270-1014. The fax phone number for the organization where this application or proceeding is assigned is 571-273-8300.
Information regarding the status of published or unpublished applications may be obtained from Patent Center. Unpublished application information in Patent Center is available to registered users. To file and manage patent submissions in Patent Center, visit: https://patentcenter.uspto.gov. Visit https://www.uspto.gov/patents/apply/patent-center for more information about Patent Center and https://www.uspto.gov/patents/docx for information about filing in DOCX format. For additional questions, contact the Electronic Business Center (EBC) at 866-217-9197 (toll-free). If you would like assistance from a USPTO Customer Service Representative, call 800-786-9199 (IN USA OR CANADA) or 571-272-1000.
/FARAZ T AKBARI/Examiner, Art Unit 2196
/APRIL Y BLAIR/Supervisory Patent Examiner, Art Unit 2196