DETAILED ACTION
Claims 1-20 are presented for examination.
Claims 1, 2, 9, 10, and 17 have been amended.
This office action is in response to the amendment submitted on 26-Mar-2026.
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 .
Examiner’s Note (EN)
The prior art rejections below cite particular paragraphs, columns, and/or line numbers in the references for the convenience of the applicant. Although the specified citations are representative of the teachings in the art and are applied to the specific limitations within the individual claim, other passages and figures may apply as well. It is respectfully requested that, in preparing responses, the applicant fully consider the references in their entirety as potentially teaching all or part of the claimed invention, as well as the context of the passage as taught by the prior art.
Claim Objections
Claims 1, 9, and 17 are objected for lack of idiomatic English, specifically the following limitation:
each of the plurality of counterexamples and in each of the plurality of states in each of the plurality of counterexamples
Appropriate correction is requested.
Response to Arguments – 35 USC 103
On pgs. 10-14 of the Applicant/Arguments Remarks (hereinafter ‘Remarks’), Applicant argues the amended claims overcome the rejection under 35 USC 103.
The applicant argues Loggozo’s verifying that a repair does not cause any additional assertion failure is not verifying the original proof.
The examiner respectfully disagrees. The original proof is a set of assertions. The re-verification process to ensure that no additional assertions fail is essentially: verifying against the original set of assertions to ensure that none of them fail in the solution being suggested. In other words, assume an original set of assertions A(O). The program initially failed a subset of A(O), SA(O). After correcting the program, Loggozo goes back and reverifies not only the subset of failed assumptions SA(O), but the entire set of assertions A(O) to ensure that there are no additional assertions that failed from the set of original assertions beyond the subset of assertions that failed.
The applicant additionally argues the Office Action asserts that because the repair in Logozzo fixes the software bug, it inherently passes the proof, this analogy fails…mere correction of a given incorrect execution of the program is not a proving of correctness of the program.
The examiner notes, as explained above, Loggozo re-verifies/proves against the original set of assertions to ensure that none of them fail. The proving is independent of the bug fixing.
Additionally, the applicant argues: Zhang fails to disclose counterexample invariants that comprise predicates that hold in all counterexamples.
The examiner points to Pg. 4, where Zhang describes an iterative loop that refines the invariants across all counterexamples to create invariants consistent with all counterexamples. “Specifically, given an existing snapshot, we mutate it with the goal of generating counterexample states that can refine the current patch invariants. For instance, given the current patch invariant (e_shnum < sect->sh_size), in the first round (SF Round_1), snapshot fuzzing generates a new state {e_shnum=32, sect->sh_size=32, ...}. This new state is a counterexample since it violates the above patch invariant but does not trigger the buffer overflow. The refined candidate invariants then guide the next round of snapshot fuzzing. This process continues until a stable solution is reached or time out.”
The applicant further argues: Zhang refers to this as a "[l]imited test suite" (FIG. 2 above) that actually teaches away from specific input values to the program code that cause the faults in the context of counterexamples.
The examiner respectfully disagrees. While Zhang evaluates the effectiveness of the fuzzy inputs and its limitations, Zhang uses fuzzy inputs as a pillar of his algorithm. However, Zhang refines the algorithm accordingly to account for the limitations of the fuzzy inputs. Zhang is in no way teaching away from inputs in the creation of counterexample invariants. In fact, the line in Pg. 4, that follows the line the applicant uses to indicate that Zhang teaches away from fuzzy input, discloses the exact point explained here. “To further refine the generated invariant, we use snapshot fuzzing to generate counterexamples by directly mutating the program states.”
As for the new limitations they’re mapped below accordingly.
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, 3-9 and 11-16 are rejected under 35 U.S.C. 103 as being unpatentable over Logozzo et al. (US20130339929A1) in view of Zhang et al. (Program Vulnerability Repair via Inductive Inference)
Regarding claim 1, Logozzo teaches a computer-implemented method for fixing a fault in a software program without executing the software program, the method comprising ([0004-0005] “An embodiment provides a method for repairing a program. The method includes statically analyzing a code of a program via a modular program verifier and determining semantic errors within the code of the program based on the static analysis. The method also includes inferring verified repairs to the code of the program based on the semantic errors. Another embodiment provides a system for repairing a program. The system includes a processor that is adapted to execute stored instructions and a system memory. The system memory includes code configured to statically analyze a code of a program, determine semantic errors within the code of the program, and, for each semantic error, generate suggested repairs to the code of the program based on a type of the semantic error”).
running a prover on program code of the software program to generate a proof, wherein the proof comprises a mathematical proving of correctness of the program code ([0004] " The method includes statically analyzing a code of a program via a modular program verifier and determining semantic errors within the code of the program based on the static analysis" [0061] “ As discussed above, the modular program verifier 304 may be an abstract interpreter or any other type of static analyzer that is capable of performing an automatic program repair procedure.” EN: [0062-0066] detail the mathematical modeling and equations used by used by the verifier/prover. [0084] “Specifically, the modular program verifier 304 may implement a goal-directed backward analysis
PNG
media_image1.png
37
29
media_image1.png
Greyscale
pc(e), starting from a failing assertion e within the program 302. For each program point pc, if
PNG
media_image1.png
37
29
media_image1.png
Greyscale
pc(e) does not hold at pc, then e will fail later in the program 302. In general,
PNG
media_image1.png
37
29
media_image1.png
Greyscale
is an under-approximation of the semantics, computing fixpoints when loops are encountered. The modular program verifier 304 may use the analysis
PNG
media_image1.png
37
29
media_image1.png
Greyscale
to suggest repairs by matching
PNG
media_image1.png
37
29
media_image1.png
Greyscale
pc(e) and the statement P(pc), as discussed further below”).
detecting, by the prover, faults in the program code as an original proof failure ([0004] " The method includes statically analyzing a code of a program via a modular program verifier and determining semantic errors within the code of the program based on the static analysis" Also [0061-0066] where the traces are traversed to construct the original proof.).
generating a set of candidate fixes ([0067] "The modular program verifier 304 may use the assertion information 312 to determine suggested repairs 318 for the program 302" and [0085-0086] “In some embodiments, repairs are performed for particular contracts of the program 302. Contracts, including preconditions, post-conditions, object invariants, assertions and assumptions, are used for code documentation. In addition, contracts may be used by the modular program verifier 304 to perform the assume/guarantee reasoning for the automatic program repair process. In various embodiments, the backward analysis procedure may be used to suggest contracts. The inference of preconditions is a form of verified repair. A candidate precondition is
PNG
media_image1.png
37
29
media_image1.png
Greyscale
entry(e). If
PNG
media_image1.png
37
29
media_image1.png
Greyscale
entry(e) meets the visibility and inheritance constraints of the enclosing method, then it can be suggested as precondition. Otherwise, it is suggested as an assumption. In both cases, P
PNG
media_image2.png
37
29
media_image2.png
Greyscale
PNG
media_image1.png
37
29
media_image1.png
Greyscale
entry(e); P follows from the fact that
PNG
media_image1.png
37
29
media_image1.png
Greyscale
only produces certain conditions”).
verifying, by the prover, that the set of candidate fixes pass the proof ([0088] "Therefore, to verify the repair before suggesting it to the user 320, the repaired program P′ 324 may be analyzed in the background to check that no additional assertion failures are introduced by the repair, so that P
PNG
media_image2.png
37
29
media_image2.png
Greyscale
a P′").
selecting a candidate fix from the set of candidate fixes that pass the proof ([0067] "The modular program verifier 304 may use the assertion information 312 to determine suggested repairs 318 for the program 302. The modular program verifier 304 may send the suggested repairs 318 to a user 320 via a graphical interface of a computing system in which the program 302 and the modular program verifier 304 reside. The user 320 may then indicate a number of accepted repairs 322 via a pointing device, for example, of the computing system").
replacing a portion of the program code that causes the original proof failure with the selected candidate fix ([0068] "Based on the accepted repairs 322, the modular program verifier 304 may repair the program 302 to generate a new, repaired program 324, denoted by P′" Additionally, [0093-0094] show the algorithm and equations for correcting semantic errors).
However, Logozzo doesn’t appear to explicitly teach:
Producing a plurality of counterexamples that illustrate the causes of the detected faults, wherein each of the plurality of counterexamples comprise specific input values to the program code that cause the faults
Wherein each of the plurality of counterexamples further comprises a plurality of states as a set of equalities between program expressions
generating a plurality of counterexample invariants, wherein each of the plurality of counterexample invariants comprise predicates that hold in each of the plurality of counterexamples and in each of the plurality of states in each of the plurality of counterexamples
Zhang teaches producing a plurality of counterexamples that illustrate the causes of the detected faults, wherein each of the plurality of counterexamples comprise specific input values to the program code that cause the faults (Pg. 3, "We propose an approach for fixing vulnerabilities based on counterexample-guided inductive inference. This helps reduce the over-fitting problem in automated program repair, without any significant deductive machinery…The workflow of inferring patch invariant is as follows: with some initial candidate invariant generated from a limited test suite (the given tests plus the tests obtained from traditional fuzzing), snapshot fuzzing attempts to invalidate the current invariant by mutating program states to find counterexamples. Given a candidate invariant, the mutation step invokes an SMT solver to obtain new values for variables that appeared in the invariant. Such mutation finds a counterexample if the program execution result is different from what the candidate invariant suggests - if a program state satisfying the candidate invariant leads to a failure in execution, this state is considered to be a counterexample to the candidate invariant…our approach is more efficient in generating counterexamples for refining the inferred invariants" Pg. 8, "The driver module (written in Python) invokes various components and communicates data (snapshots, patch invariants) between them. It processes the snapshots produced by the instrumentation code and classifies them based on the program execution status. It also implements the core of snapshot fuzzing for generating counterexample snapshots based on the given patch invariants and test inputs" Pg. 10, "This workflow is conceptually similar to counterexample-guided inductive synthesis (CEGIS), i.e., infer initial candidates and then generate new test inputs (counterexample) to rule out incorrect candidates").
Wherein each of the plurality of counterexamples further comprises a plurality of states as a set of equalities between program expressions (Pg. 4, “Specifically, given an existing snapshot, we mutate it with the goal of generating counterexample states that can refine the current patch invariants. For instance, given the current patch invariant (e_shnum < sect->sh_size), in the first round (SF Round_1), snapshot fuzzing generates a new state {e_shnum=32, sect->sh_size=32, ...}. This new state is a counterexample since it violates the above patch invariant but does not trigger the buffer overflow. The refined candidate invariants then guide the next round of snapshot fuzzing. This process continues until a stable solution is reached or time out.” Pg. 3, “Given a candidate invariant, the mutation step invokes an SMT solver to obtain new values for variables that appeared in the invariant. Such mutation finds a counterexample if the program execution result is different from what the candidate invariant suggests - if a program state satisfying the candidate invariant leads to a failure in execution, this state is considered to be a counterexample to the candidate invariant. These new counterexample program states are then used to refine the candidate invariant, which in turn guides the next round of mutation.” EN: SMT (Satisfiability Modulo Theories) solver uses mathematical formulas and equalities)
generating a plurality of counterexample invariants, wherein each of the plurality of counterexample invariants comprise predicates that hold in each of the plurality of counterexamples and in each of the plurality of states in each of the plurality of counterexamples (Please see Fig. 2 and Pg. 3, "To address the above challenges, we propose snapshot fuzzing to efficiently explore program states with the goal of inferring precise patch invariants. Specifically, instead of mutating the test inputs at the entry point of a program, snapshot fuzzing heuristically mutates the program state (i.e., snapshot) at certain program points. We remark that these mutated program states may not be reachable from the beginning of the program, and the patch invariant is inferred using both feasible and infeasible program states. The impact of infeasible states on our patch invariants is not significant, and it is examined in detail in Section 3.2. The workflow of inferring patch invariant is as follows: with some initial candidate invariant generated from a limited test suite (the given tests plus the tests obtained from traditional fuzzing), snapshot fuzzing attempts to invalidate the current invariant by mutating program states to find counterexamples. Given a candidate invariant, the mutation step invokes an SMT solver to obtain new values for variables that appeared in the invariant. Such mutation finds a counterexample if the program execution result is different from what the candidate invariant suggests - if a program state satisfying the candidate invariant leads to a failure in execution, this state is considered to be a counterexample to the candidate invariant. These new counterexample program states are then used to refine the candidate invariant, which in turn guides the next round of mutation" Pg. 4, “Specifically, given an existing snapshot, we mutate it with the goal of generating counterexample states that can refine the current patch invariants. For instance, given the current patch invariant (e_shnum < sect->sh_size), in the first round (SF Round_1), snapshot fuzzing generates a new state {e_shnum=32, sect->sh_size=32, ...}. This new state is a counterexample since it violates the above patch invariant but does not trigger the buffer overflow. The refined candidate invariants then guide the next round of snapshot fuzzing. This process continues until a stable solution is reached or time out.”).
PNG
media_image3.png
329
600
media_image3.png
Greyscale
Logozzo and Zhang are analogous art because they are from the same field of endeavor in static code analysis and repair. Before the effective filing date of the invention, it would have been obvious to a person of ordinary skill in the art, to combine Logozzo and Zhang to incorporate Zhang’s counterexample workflow to generate more robust fixes that cover a wide range of errors. “As compared to proposed approaches for vulnerability repair such as CPR or SenX which are based on concolic and symbolic execution respectively, we can repair significantly more vulnerabilities.” (Zhang, Abstract).
Regarding claim 3, Logozzo in view of Zhang teaches the method of claim 1. Logozzo further teaches wherein the set of candidate fixes comprises implementation fixes and generating the set of candidate fixes comprises selecting a fix schema that abstracts common instruction patterns and instantiating the fix schema ([0103] "In some embodiments, the verified repairs are inferred based on the particular types of semantic errors that are identified. For example, a specific template or method may be used to infer verified repairs for contract errors, while a different template or method may be used to infer verified repairs for floating point comparison errors, as discussed above with respect to FIG. 3" and [0093-0096] "The algorithm may be a non-deterministic memorization-based algorithm that is defined by a set of rewriting rules, which are shown below in Eqs. 9-25." Please refer to Eqs. 9-25 for the rewriting rules).
Regarding claim 4, Logozzo in view of Zhang teaches the method of claim 3. Logozzo further teaches wherein the instantiated fix schema replaces an instruction at a location of a fault ([0096] "In addition, the algorithm is an abstract interpretation of the trivial algorithm, which enumerates all the equivalent expressions and then checks for non-overflowing. According to the rules above, a constant, a variable, and the comparison of non-overflowing expressions do not overflow. The uncertainty on a binary arithmetic expression can be removed if the underlying abstract state guarantees that the operation does not overflow. Moving the right operand of a subtraction to the right of a comparison operator removes a possible overflow. In the case of an addition, −a does not overflow, i.e., a may be MinInt. Division by a constant overflows if k=0 or if MinInt is divided by −1. Half-sum can be written in two ways. An addition can be traded for a subtraction, or a subtraction can be traded for an addition if the new expression does not overflow. Finally, shuffling expressions may be allowed by moving them on the same side of a relational operator, and strict inequalities may be introduced to remove overflows. Let P′ be such that all the overflowing expressions are replaced by the result of the algorithm above. Then P
PNG
media_image2.png
37
29
media_image2.png
Greyscale
a P′.").
Regarding claim 5, Logozzo in view of Zhang teaches the method of claim 1. Logozzo further teaches wherein the prover is configured for mistake detection and fix validation and mistake detection and fix validation do not use test cases ([0023] "The method and system described herein use semantic static analysis techniques to detect possible software bugs, e.g., semantic errors, within the code of a particular program. The semantic static analysis techniques may be performed statically, meaning that the techniques may be performed without executing the program. In addition, the method and system described herein may provide for automatic repairing of the program by suggesting one or more code repairs for the possible software bug." [0100] "The method begins at block 402, at which the code of a program is statically analyzed via the modular program verifier. More specifically, the execution traces within the program code may be analyzed. In various embodiments, the program is analyzed without being executed. For example, the program may be analyzed during the development stage, even if the program has not been completed").
Regarding claim 6, Logozzo in view of Zhang teaches the method of claim 5. Logozzo further teaches wherein the replacing the portion of the program code that causes the first mistake takes place automatically when a candidate fix is selected ([0068] "Based on the accepted repairs 322, the modular program verifier 304 may repair the program 302 to generate a new, repaired program 324, denoted by P′").
Regarding claim 7, Logozzo in view of Zhang teaches the method of claim 6. Logozzo further teaches wherein the candidate fix is selected automatically by the fixing tool (0097] "In some embodiments, before sending the suggested repairs 318 to the user 320, the modular program verifier 304 performs a simplification procedure to eliminate any redundant repairs. For example, if x>0 and x>1 are inferred as suggested repairs 318, the modular program verifier 304 may retain only the latter repair. Because several repairs are often generated for one warning, such a simplification procedure may be frequently used to simplify the automatic program repair process").
Regarding claim 8, Logozzo in view of Zhang teaches the method of claim 1. Logozzo further teaches wherein the detected faults are not limited to any particular type ([0046] "The automatic program repair techniques described herein may be used to implement any of a number of different types of program repairs. For example, in some cases, the code of a method is correct only when executed under certain conditions. In such cases, a program repair may be performed to introduce a contract including appropriate preconditions and/or post-conditions. As shown in the following code fragment, when a parameter is null, there will be a failure due to a null deference of the parameter." [0103] "In some embodiments, the verified repairs are inferred based on the particular types of semantic errors that are identified. For example, a specific template or method may be used to infer verified repairs for contract errors, while a different template or method may be used to infer verified repairs for floating point comparison errors, as discussed above with respect to FIG. 3").
Regarding claim 9, Logozzo teaches A system for identifying and fixing a fault in program code, the system comprising:
at least one processor operably coupled to memory, and instructions that, when executed by the at least one processor, cause the at least one processor to implement ([0005] “Another embodiment provides a system for repairing a program. The system includes a processor that is adapted to execute stored instructions and a system memory. The system memory includes code configured to statically analyze a code of a program, determine semantic errors within the code of the program, and, for each semantic error, generate suggested repairs to the code of the program based on a type of the semantic error”).
Zhang teaches an invariant inferencer configured to (Please see fig. 2)
PNG
media_image3.png
329
600
media_image3.png
Greyscale
The remaining limitations are similar to claim 1 and are rejected under the same rationale.
Claims 11-16 are system claims that recite limitations similar to claims 3-8 respectively and are rejected under the same rationale.
Claims 2, 10, and 17-20 are rejected under 35 U.S.C. 103 as being unpatentable over Logozzo et al. (US20130339929A1) in view of Zhang et al. (Program Vulnerability Repair via Inductive Inference) further in view of Certora (GitHub: Vacuous Rules and Invariants)
Regarding claim 2, Logozzo in view of Zhang teaches the method of claim 1. Logozzo further teaches wherein the set of candidate fixes comprises contract fixes affecting the specification of a routine of the program code ([0025-0026] "According to embodiments described herein, a modular program verifier uses contracts, e.g., preconditions, post-conditions, object invariants and assumptions, to decompose the verification problem from the level of a whole program to the level of individual methods. Developer-supplied contracts are essential not only for scalability, but also for documenting intent as well as localizing the cause of failures. The modular program verifier described herein may be an abstract interpreter or any other type of static analyzer. The modular program verifier may be used to generate repairs for contract violations and runtime errors. More specifically, the modular program verifier may be used to generate repairs for missing contracts, e.g., missing preconditions, post-conditions, object invariants, or assumptions, as well as incorrect initialization and conditionals, e.g., wrong constraints or buffer sizes, guards, e.g., negation, strengthening, or weakening, buffer overflows, arithmetic overflows, incorrect floating point comparisons, or the like" and [0103] “In some embodiments, the verified repairs are inferred based on the particular types of semantic errors that are identified. For example, a specific template or method may be used to infer verified repairs for contract errors, while a different template or method may be used to infer verified repairs for floating point comparison errors, as discussed above with respect to FIG. 3”).
However, Logozzo and Zhang don’t appear to teach:
selecting the candidate fix further comprises injecting a fault into the routine by inserting a contradictory assertion
Certora teaches selecting the candidate fix further comprises injecting a fault into r by inserting a contradictory assertion (Pg. 2-3, “Adding assert false: By adding an assert false to the last line of a rule and expecting it to fail, we're asking the question - "Is there a path (set of values) that reached our original last assert and passed it?". When we fail the newly added assert, the answer to our question is "Yes - there is a set of values that reached and passed our last original assert". If all paths were to revert before reaching our assert false, this assert will have never been checked in the first place").
Logozzo, Zhang and Certora are analogous art because they are from the same field of endeavor in static code analysis, verification and repair. Before the effective filing date of the invention, it would have been obvious to a person of ordinary skill in the art, to combine Logozzo, Zhang and Certora to incorporate false assertion insertion as an additional validation step to further validate generated fixes and ensure they’re not vacuous fixes. This is combining a known verification technique to a known repair-verification framework thereby yielding predictable results and improving the resultant candidate fixes. “Vacuous rules are extremely dangerous since they create false confidence in the properties of the system, which can lead to a premature deployment of a set of contracts. Vacuous rules are way more common than you might think. When writing complex rules and invariants, it is easy to lose track and require too many assumptions. Sometimes these requirements may eliminate every possible route so that the assertion will never be reached (the ultimate under-approximation).” (Certora, Pg. 1).
Regarding claim 10 is a system claim that recites limitations similar to claim 2 and is rejected under the same rationale.
Regarding claim 17, Logozzo teaches a computer-implemented method for selecting a fix for an mistake in program code without executing the program code, the method comprising ([0004-0005] “An embodiment provides a method for repairing a program. The method includes statically analyzing a code of a program via a modular program verifier and determining semantic errors within the code of the program based on the static analysis. The method also includes inferring verified repairs to the code of the program based on the semantic errors. Another embodiment provides a system for repairing a program. The system includes a processor that is adapted to execute stored instructions and a system memory. The system memory includes code configured to statically analyze a code of a program, determine semantic errors within the code of the program, and, for each semantic error, generate suggested repairs to the code of the program based on a type of the semantic error” and [0067] "The modular program verifier 304 may use the assertion information 312 to determine suggested repairs 318 for the program 302. The modular program verifier 304 may send the suggested repairs 318 to a user 320 via a graphical interface of a computing system in which the program 302 and the modular program verifier 304 reside. The user 320 may then indicate a number of accepted repairs 322 via a pointing device, for example, of the computing system").
running a prover on the program code to generate a proof, wherein the proof comprises a mathematical proving of correctness of the program code ([0004] and [0061-0066]).
detecting, by the prover, faults in the program code ([0004] and [0061-0066]).
generating a set of candidate fixes ([0067] "The modular program verifier 304 may use the assertion information 312 to determine suggested repairs 318 for the program 302" and [0085-0086] “In some embodiments, repairs are performed for particular contracts of the program 302. Contracts, including preconditions, post-conditions, object invariants, assertions and assumptions, are used for code documentation. In addition, contracts may be used by the modular program verifier 304 to perform the assume/guarantee reasoning for the automatic program repair process. In various embodiments, the backward analysis procedure may be used to suggest contracts. The inference of preconditions is a form of verified repair. A candidate precondition is
PNG
media_image1.png
37
29
media_image1.png
Greyscale
entry(e). If
PNG
media_image1.png
37
29
media_image1.png
Greyscale
entry(e) meets the visibility and inheritance constraints of the enclosing method, then it can be suggested as precondition. Otherwise, it is suggested as an assumption. In both cases, P
PNG
media_image2.png
37
29
media_image2.png
Greyscale
PNG
media_image1.png
37
29
media_image1.png
Greyscale
entry(e); P follows from the fact that
PNG
media_image1.png
37
29
media_image1.png
Greyscale
only produces certain conditions”).
verifying, by the prover, that the set of candidate fixes pass the proof ([0088] "Therefore, to verify the repair before suggesting it to the user 320, the repaired program P′ 324 may be analyzed in the background to check that no additional assertion failures are introduced by the repair, so that P
PNG
media_image2.png
37
29
media_image2.png
Greyscale
a P′").
However, Logozzo doesn’t appear to explicitly teach:
producing a set of counterexamples that illustrate the causes of the detected faults; wherein each counterexample in the set of the counterexamples comprises specific input values to the program code that cause the faults, wherein each counterexample in the set of counterexamples further comprises a plurality of states as a set of equalities between program expressions
generating counterexample invariants, wherein each of the counterexample invariants comprise predicates that hold in each of the plurality of counterexamples and in each of the plurality of states in each of the plurality of counterexamples
filtering spurious fixes by injecting a fault into a plurality of candidate fixes
selecting a candidate fix from the set of candidate fixes that pass the proof and discarding the candidate fixes with which the prover fails to detect the injected fault
Zhang teaches producing a set of counterexamples that illustrate the causes of the detected faults; wherein each counterexample in the set of the counterexamples comprises specific input values to the program code that cause the faults (Pg. 3, "We propose an approach for fixing vulnerabilities based on counterexample-guided inductive inference. This helps reduce the over-fitting problem in automated program repair, without any significant deductive machinery." Pg. 8, "The driver module (written in Python) invokes various components and communicates data (snapshots, patch invariants) between them. It processes the snapshots produced by the instrumentation code and classifies them based on the program execution status. It also implements the core of snapshot fuzzing for generating counterexample snapshots based on the given patch invariants and test inputs" Pg. 10, "This workflow is conceptually similar to counterexample-guided inductive synthesis (CEGIS), i.e., infer initial candidates and then generate new test inputs (counterexample) to rule out incorrect candidates").
Wherein each of the plurality of counterexamples further comprises a plurality of states as a set of equalities between program expressions (Pg. 4, “Specifically, given an existing snapshot, we mutate it with the goal of generating counterexample states that can refine the current patch invariants. For instance, given the current patch invariant (e_shnum < sect->sh_size), in the first round (SF Round_1), snapshot fuzzing generates a new state {e_shnum=32, sect->sh_size=32, ...}. This new state is a counterexample since it violates the above patch invariant but does not trigger the buffer overflow. The refined candidate invariants then guide the next round of snapshot fuzzing. This process continues until a stable solution is reached or time out.” Pg. 3, “Given a candidate invariant, the mutation step invokes an SMT solver to obtain new values for variables that appeared in the invariant. Such mutation finds a counterexample if the program execution result is different from what the candidate invariant suggests - if a program state satisfying the candidate invariant leads to a failure in execution, this state is considered to be a counterexample to the candidate invariant. These new counterexample program states are then used to refine the candidate invariant, which in turn guides the next round of mutation.” EN: SMT (Satisfiability Modulo Theories) solver uses mathematical formulas and equalities)
generating counterexample invariants, wherein each of the counterexample invariants comprise predicates that hold in each of the plurality of counterexamples and in each of the plurality of states in each of the plurality of counterexamples (Please see Fig. 2 and Pg. 3, "To address the above challenges, we propose snapshot fuzzing to efficiently explore program states with the goal of inferring precise patch invariants. Specifically, instead of mutating the test inputs at the entry point of a program, snapshot fuzzing heuristically mutates the program state (i.e., snapshot) at certain program points. We remark that these mutated program states may not be reachable from the beginning of the program, and the patch invariant is inferred using both feasible and infeasible program states. The impact of infeasible states on our patch invariants is not significant, and it is examined in detail in Section 3.2. The workflow of inferring patch invariant is as follows: with some initial candidate invariant generated from a limited test suite (the given tests plus the tests obtained from traditional fuzzing), snapshot fuzzing attempts to invalidate the current invariant by mutating program states to find counterexamples. Given a candidate invariant, the mutation step invokes an SMT solver to obtain new values for variables that appeared in the invariant. Such mutation finds a counterexample if the program execution result is different from what the candidate invariant suggests - if a program state satisfying the candidate invariant leads to a failure in execution, this state is considered to be a counterexample to the candidate invariant. These new counterexample program states are then used to refine the candidate invariant, which in turn guides the next round of mutation" Pg. 4, “Specifically, given an existing snapshot, we mutate it with the goal of generating counterexample states that can refine the current patch invariants. For instance, given the current patch invariant (e_shnum < sect->sh_size), in the first round (SF Round_1), snapshot fuzzing generates a new state {e_shnum=32, sect->sh_size=32, ...}. This new state is a counterexample since it violates the above patch invariant but does not trigger the buffer overflow. The refined candidate invariants then guide the next round of snapshot fuzzing. This process continues until a stable solution is reached or time out.”).
filtering spurious fixes
selecting a candidate fix from the set of candidate fixes that pass the proof and discarding the candidate fixes with results of CPR are shown in the “CPR” columns in Table 2. Column “Rank” shows the rank of the correct patch in the final patch pool. Column “Ratio” shows the patch pool reduction ratio, which is the percentage of initial patches that are discarded by co-exploration of the patch space and input space … VulnFix performs snapshot mutation to discard overfitting patch invariants”).
PNG
media_image3.png
329
600
media_image3.png
Greyscale
Logozzo and Zhang are analogous art because they are from the same field of endeavor in static code analysis and repair. Before the effective filing date of the invention, it would have been obvious to a person of ordinary skill in the art, to combine Logozzo and Zhang to incorporate Zhang’s counterexample workflow to generate more robust fixes that cover a wide range of errors. “As compared to proposed approaches for vulnerability repair such as CPR or SenX which are based on concolic and symbolic execution respectively, we can repair significantly more vulnerabilities.” (Zhang, Abstract).
However, Logozzo and Zhang don’t appear to explicitly teach:
by injecting a fault into a plurality of candidate fixes
the prover fails to detect the injected fault
Certora teaches by injecting a fault into a plurality of candidate fixes (Pg. 1, “Once a rule/invariant we've written has passed, we should use either of the following two methods to check it's not vacuous. Adding assert false - By adding an assert false to the last line of a rule and expecting it to fail, we're asking the question - "Is there a path (set of values) that reached our original last assert and passed it?". When we fail the newly added assert, the answer to our question is "Yes - there is a set of values that reached and passed our last original assert". If all paths were to revert before reaching our assert false, this assert will have never been checked in the first place”).
the prover fails to detect the injected fault (Pg. 1, “This rule calls every function in the contract and then assert false. It tries to capture vacuous functions in the contract. The results we get should always be thumbs down since assert false will always throw a violation. However, if the contract itself has a function that reverts every time it's being called regardless of input, then the function is vacuous, alerting the developers (because it does nothing)”).
Logozzo, Zhang and Certora are analogous art because they are from the same field of endeavor in static code analysis, verification and repair. Before the effective filing date of the invention, it would have been obvious to a person of ordinary skill in the art, to combine Logozzo, Zhang and Certora to incorporate false assertion insertion as an additional validation step to further validate generated fixes and ensure they’re not vacuous fixes. This is combining a known verification technique to a known repair-verification framework thereby yielding predictable results and improving the resultant candidate fixes. “Vacuous rules are extremely dangerous since they create false confidence in the properties of the system, which can lead to a premature deployment of a set of contracts. Vacuous rules are way more common than you might think. When writing complex rules and invariants, it is easy to lose track and require too many assumptions. Sometimes these requirements may eliminate every possible route so that the assertion will never be reached (the ultimate under-approximation).” (Certora, Pg. 1).
Regarding claim 18, Logozzo in view of Zhang and further in view of Certora teaches the method of claim 17. Logozzo further teaches wherein the prover is used for mistake detection and fix validation and mistake detection and fix validation do not use test cases ([0023] "The method and system described herein use semantic static analysis techniques to detect possible software bugs, e.g., semantic errors, within the code of a particular program. The semantic static analysis techniques may be performed statically, meaning that the techniques may be performed without executing the program. In addition, the method and system described herein may provide for automatic repairing of the program by suggesting one or more code repairs for the possible software bug." [0100] "The method begins at block 402, at which the code of a program is statically analyzed via the modular program verifier. More specifically, the execution traces within the program code may be analyzed. In various embodiments, the program is analyzed without being executed. For example, the program may be analyzed during the development stage, even if the program has not been completed").
Regarding claim 19, Logozzo in view of Zhang and further in view of Certora teaches the method of claim 17. Logozzo further teaches wherein the replacing a portion of the program code that causes the first mistake takes place automatically when a candidate fix is selected ([0068] "Based on the accepted repairs 322, the modular program verifier 304 may repair the program 302 to generate a new, repaired program 324, denoted by P′").
Regarding claim 20, Logozzo in view of Zhang and further in view of Certora teaches the method of claim 17. Logozzo further teaches The method of claim 19, wherein the candidate fix is selected manually or automatically ([0067] "The modular program verifier 304 may use the assertion information 312 to determine suggested repairs 318 for the program 302. The modular program verifier 304 may send the suggested repairs 318 to a user 320 via a graphical interface of a computing system in which the program 302 and the modular program verifier 304 reside. The user 320 may then indicate a number of accepted repairs 322 via a pointing device, for example, of the computing system" [0102] "At block 406, verified repairs to the code of the program are inferred based on the semantic errors. The modular program verifier may then send the verified repairs to a user of the computing device on which the program resides. In some embodiments, a number of verified repairs are determined for each semantic error, and a user may be allowed to select a particular verified repair to implement for each semantic error").
Conclusion
The prior art made of record and not relied upon is considered pertinent to applicant's disclosure.
Li et al. (Improving Counterexample Quality from Failed Program Verification): discloses fault injection to improve counterexample generation.
Gao et al. (Program Repair): discloses a survey of available methods of static analysis in the field of program repair.
Deline et al. (US-20140096112-A1): discloses fault injection to ascertain the prover is valid.
THIS ACTION IS MADE FINAL. Applicant is reminded of the extension of time policy as set forth in 37 CFR 1.136(a).
A shortened statutory period for reply to this final action is set to expire THREE MONTHS from the mailing date of this action. In the event a first reply is filed within TWO MONTHS of the mailing date of this final action and the advisory action is not mailed until after the end of the THREE-MONTH shortened statutory period, then the shortened statutory period will expire on the date the advisory action is mailed, and any nonprovisional extension fee (37 CFR 1.17(a)) pursuant to 37 CFR 1.136(a) will be calculated from the mailing date of the advisory action. In no event, however, will the statutory period for reply expire later than SIX MONTHS from the mailing date of this final action.
Any inquiry concerning this communication or earlier communications from the examiner should be directed to AMIR DARWISH whose telephone number is (571)272-4779. The examiner can normally be reached 7:30-5:30 M-Thurs.
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, Lewis Bullock can be reached on 571-272-3759. 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.
/A.E.D./Examiner, Art Unit 2199
/LEWIS A BULLOCK JR/Supervisory Patent Examiner, Art Unit 2199
Prosecution Insights