CTNF 18/722,874 CTNF 99697 DETAILED ACTION This action is in response to the claims filed June 21, 2024. Claims 1-11 are pending. Claim 1 is an independent claim. Notice of Pre-AIA or AIA Status 07-03-aia AIA 15-10-aia The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA. Claim Objections 07-29-01 AIA Claim s 2 and 3 are objected to because of the following informalities: - Claim 2 recites “if not” and “else” on lines 5 and 7. This should likely read “if the initial symbolic representation of the software instruction does not comprise the symbolic expression of a read or a write operation” and “if the initial symbolic representation of the software instruction comprises the symbolic expression of a read or a write operation” respectively. - Claim 3 reads “wherein an abstract domain representing an abstract value attached to a variable or to an expression of the computer program”. This should likely read “wherein an abstract domain represents an abstract value attached to a variable or to an expression of the computer program . Appropriate correction is required. 07-30-03-h AIA Claim Interpretation 07-30-03 AIA The following is a quotation of 35 U.S.C. 112(f): (f) Element in Claim for a Combination. – An element in a claim for a combination may be expressed as a means or step for performing a specified function without the recital of structure, material, or acts in support thereof, and such claim shall be construed to cover the corresponding structure, material, or acts described in the specification and equivalents thereof. The following is a quotation of pre-AIA 35 U.S.C. 112, sixth paragraph: An element in a claim for a combination may be expressed as a means or step for performing a specified function without the recital of structure, material, or acts in support thereof, and such claim shall be construed to cover the corresponding structure, material, or acts described in the specification and equivalents thereof. 07-30-05 The claims in this application are given their broadest reasonable interpretation using the plain meaning of the claim language in light of the specification as it would be understood by one of ordinary skill in the art. The broadest reasonable interpretation of a claim element (also commonly referred to as a claim limitation) is limited by the description in the specification when 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, is invoked. As explained in MPEP § 2181, subsection I, claim limitations that meet the following three-prong test will be interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph: (A) the claim limitation uses the term “means” or “step” or a term used as a substitute for “means” that is a generic placeholder (also called a nonce term or a non-structural term having no specific structural meaning) for performing the claimed function; (B) the term “means” or “step” or the generic placeholder is modified by functional language, typically, but not always linked by the transition word “for” (e.g., “means for”) or another linking word or phrase, such as “configured to” or “so that”; and (C) the term “means” or “step” or the generic placeholder is not modified by sufficient structure, material, or acts for performing the claimed function. Use of the word “means” (or “step”) in a claim with functional language creates a rebuttable presumption that the claim limitation is to be treated in accordance with 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph. The presumption that the claim limitation is interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, is rebutted when the claim limitation recites sufficient structure, material, or acts to entirely perform the recited function. Absence of the word “means” (or “step”) in a claim creates a rebuttable presumption that the claim limitation is not to be treated in accordance with 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph. The presumption that the claim limitation is not interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, is rebutted when the claim limitation recites function without reciting sufficient structure, material or acts to entirely perform the recited function. Claim limitations in this application that use the word “means” (or “step”) are being interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, except as otherwise indicated in an Office action. Conversely, claim limitations in this application that do not use the word “means” (or “step”) are not being interpreted under 35 U.S.C. 112(f) or pre-AIA 35 U.S.C. 112, sixth paragraph, except as otherwise indicated in an Office action. Specifically, claim 10 recites “A system comprising means adapted to carry out the steps of the method according to claim 1”. The claim recites the term “means”, modifies it with functional language “adapted to carry out”, and does not recite sufficient structure, material, or acts to perform the claimed function. Therefore, claim 10 is interpreted under 35 U.S.C. 112(f). Claim Rejections - 35 USC § 101 07-04-01 AIA 07-04 35 U.S.C. 101 reads as follows: Whoever invents or discovers any new and useful process, machine, manufacture, or composition of matter, or any new and useful improvement thereof, may obtain a patent therefor, subject to the conditions and requirements of this title. Claims 1-11 rejected under 35 U.S.C. 101 because the claimed invention is directed to an abstract idea without significantly more. Regarding claim 1, the limitations “analyzing an initial symbolic representation of a software instruction to determine if a simplification may be applied to any memory-access operation included in the initial symbolic representation of the software instruction”, “in case of determining a simplification, generating a simplified symbolic representation of said software instruction to replace the initial symbolic representation”, and “generating a new symbolic representation of the computer program with the simplified symbolic representation of said software instruction” as drafted, are functions that, under their broadest reasonable interpretation, recite the abstract idea of a mental process. The limitation encompasses a human mind carrying out the function through observation, evaluation, judgement, and/or opinion, or even with the aid of pen and paper. Thus, these limitations recite and call under the “Mental Processes” grouping of abstract ideas under Prong 1. Under Prong 2, this judicial exception is not integrated into a practical application. The additional element “A computer implemented method for performing symbolic execution on a symbolic representation of a computer program comprising a sequence of software instructions represented at least by variables, memories and expressions, the method being operated on-the-fly and comprising for each software instruction of the computer program” is recited at a high level of generality such that it amounts to no more than mere instructions to apply the exception using a generic computer, and/or mere computer components. See MPEP 2106.05(f). Accordingly, the additional elements do not integrate the recited judicial exception into a practical application and the claim is therefore directed to the judicial exception. Under Step 2B, the claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional element of “A computer implemented method for performing symbolic execution on a symbolic representation of a computer program comprising a sequence of software instructions represented at least by variables, memories and expressions, the method being operated on-the-fly and comprising for each software instruction of the computer program” amounts to no more than mere instructions, or generic computer/computer components to carry out the exception. See MPEP 2106.05(f). Accordingly, the claims are not patent eligible under 35 U.S.C. 101. Regarding claim 2, the limitations “wherein the step of analyzing an initial symbolic representation of a software instruction comprises”, “determining if the initial symbolic representation of the software instruction comprises a symbolic expression of a read or a write operation”, and “else, processing the symbolic expression of the read operation or of the write operation” are additional mental steps. Claim 2 does not recite additional limitations which amount to practical application under Prong 2, nor amount to significantly more under Step 2B. Regarding claim 3, the limitation “wherein the analyzing step comprises using context mapping information to determine if a simplification may be applied to the initial symbolic representation of the software instruction, wherein context mapping information is information on previous computations made with variables and memories included in the sequence of software instructions, and information on previous computed abstract domains wherein an abstract domain representing an abstract value attached to a variable or to an expression of the computer program” is an additional mental step. Claim 3 does not recite additional limitations which amount to practical application under Prong 2, nor amount to significantly more under Step 2B. Regarding claim 4, the limitation “further comprising a step of updating abstract domains of the context mapping according to abstract domains of the initial symbolic representation of the software instruction” is an additional mental step. Claim 4 does not recite additional limitations which amount to practical application under Prong 2, nor amount to significantly more under Step 2B. Regarding claim 5, the limitation “wherein the step of analyzing the initial symbolic representation of a software instruction further comprises a step of reducing the number of memory access” is an additional mental step. Claim 5 does not recite additional limitations which amount to practical application under Prong 2, nor amount to significantly more under Step 2B. Regarding claim 6, the limitations “wherein the step of reducing the number of memory access comprises the steps of determining:”, “that the symbolic representation of the software instruction is either a write operation (store(M,Addr,Val)) or a read operation (load(M, Addr)), with the address of the software instruction being an expression in the form "X+k" of a variable and a constant k”, “that the context mapping contains an expression in the form "X --> Y+k" of a variable Y and a constant k' for the address X”, and “to replace the expression of the address in the current symbolic representation of the software instruction by a new expression in the form "Y + (k+k')", thereby generating a new symbolic representation of the software instruction, in the form of "store(M,Y+(k+k),Val)" for the write operation or in the form of "load(M, Y+(k+k'))" for the read operation” is an additional mental step. Claim 6 does not recite additional limitations which amount to practical application under Prong 2, nor amount to significantly more under Step 2B. Regarding claim 7, the limitation “further comprising a step of updating the context mapping with the new expression” is an additional mental step. Claim 7 does not recite additional limitations which amount to practical application under Prong 2, nor amount to significantly more under Step 2B. Regarding claim 8, the limitation “wherein the step of reducing the number of memory access comprises the steps of determining that the received instruction is in the form “ X: = load (M’, a’)” of a load of a value a' to a memory M', and that the current context mapping contains an expression for the memory M' defined in the received instruction, to generate a simplified symbolic representation of said software instruction to replace the initial symbolic representation” is an additional mental step. Claim 8 does not recite additional limitations which amount to practical application under Prong 2, nor amount to significantly more under Step 2B. Regarding claim 9, the limitation “further comprising before generating a simplified symbolic representation of said software instruction, a step of determining if the value a' in the load instruction is equal to a value a defined in the expression of the current context mapping” is an additional mental step. Claim 9 does not recite additional limitations which amount to practical application under Prong 2, nor amount to significantly more under Step 2B. Regarding claim 10, the limitation “A system comprising means adapted to carry out the steps of the method according to claim 1” uses “A system” to complete the mental steps recited in claim 1. Under Prong 2, the limitation is recited at a high level of generality such that it amounts to no more than mere instructions to apply the exception using a generic computer, and/or mere computer components. Therefore, the claim does not integrate the judicial exception into a practical application. See MPEP 2106.05(f). Under Step 2B, the limitation amounts to no more than mere instructions, or generic computer/computer components to carry out the exception. Therefore, the claim does not amount to significantly more than the judicial exception. See MPEP 2106.05(f). Regarding claim 11, the limitation “A computer program comprising instructions for carrying out the steps of the method according to claim 1 when said computer program is executed on a suitable computer device” uses “a computer program comprising instructions” on a “computer device” to complete the mental steps recited in claim 1. Under Prong 2, the limitation is recited at a high level of generality such that it amounts to no more than mere instructions to apply the exception using a generic computer, and/or mere computer components. Therefore, the claim does not integrate the judicial exception into a practical application. See MPEP 2106.05(f). Under Step 2B, the limitation amounts to no more than mere instructions, or generic computer/computer components to carry out the exception. Therefore, the claim does not amount to significantly more than the judicial exception. See MPEP 2106.05(f). Claim 11 is rejected under 35 U.S.C. 101 because the claimed invention is directed to non-statutory subject matter. Claim 11 is directed to a computer program. However, the recited components of the computer program appear to lack the necessary physical components (hardware) to constitute a machine or manufacture under § 101. The recited components of the system can be construed to cover software under the broadest reasonable interpretation. Therefore, the claimed system is ineligible subject matter under § 101. Claim Rejections - 35 USC § 102 07-06 AIA 15-10-15 In the event the determination of the status of the application as subject to AIA 35 U.S.C. 102 and 103 (or as subject to pre-AIA 35 U.S.C. 102 and 103) is incorrect, any correction of the statutory basis (i.e., changing from AIA to pre-AIA) for the rejection will not be considered a new ground of rejection if the prior art relied upon, and the rationale supporting the rejection, would be the same under either status. 07-07-aia AIA 07-07 The following is a quotation of the appropriate paragraphs of 35 U.S.C. 102 that form the basis for the rejections under this section made in this Office action: A person shall be entitled to a patent unless – 07-12-aia AIA (a)(2) the claimed invention was described in a patent issued under section 151, or in an application for patent published or deemed published under section 122(b), in which the patent or application, as the case may be, names another inventor and was effectively filed before the effective filing date of the claimed invention. 07-15-03-aia AIA Claim s 1, 5, 10, and 11 are rejected under 35 U.S.C. 102(a)(2) as being anticipated by “BINSEC/REL: Efficient Relational Symbolic Execution for Constant-Time and Binary Level” by Daniel et. al (hereinafter “Daniel”) . Regarding claim 1, Daniel discloses: A computer implemented method for performing symbolic execution on a symbolic representation of a computer program comprising a sequence of software instructions represented at least by variables, memories and expressions, the method being operated on-the-fly and comprising for each software instruction of the computer program (Page 1023, “Symbolic Execution (SE) [37], [38], [56] consists in executing a program on symbolic inputs instead of concrete input values. Variables and expressions of the program are represented as terms over symbolic inputs and the current path is modeled by a path predicate (a logical formula), which is the conjunction of conditional expressions encountered along the execution”; Page 1027, “Relational symbolic execution does not scale in the context of binary-level analysis (see RelSE in Table V). In order to achieve better scalability, we enrich our analysis with an optimization, called on-the-fly-read-over-write (FlyRow in Table VI), based on read-over-write [66]. This optimization simplifies expressions and resolves load operations ahead of the solver, often avoiding to resort to the duplicated memory and allowing to spare insecurity queries. We also enrich our analysis with two further optimizations, called untainting and fault-packing (Unt and fp in Table VI), specifically targeting SE for information flow analysis”) [Examiner’s remarks: Daniel discloses an on-the-fly operation which performs analysis of symbolic execution on a symbolic representation with at least variables, memories, and expressions.] : - analyzing an initial symbolic representation of a software instruction to determine if a simplification may be applied to any memory-access operation included in the initial symbolic representation of the software instruction (Page 1025, “To mitigate this issue, we propose dedicated simplifications for binary-level relational symbolic execution that allow a precise tracking of secret-dependencies in the memory (details in Section V-A). In the particular example of Table I, our prototype BINSEC/REL does prove that the code is secure in less than 20 minutes. Our simplifications simplify all the queries, resulting in a ×2000 speedup compared to standard RelSE and SC in terms of number of instructions treated per second”; Page 1027, “Relational symbolic execution does not scale in the context of binary-level analysis (see RelSE in Table V). In order to achieve better scalability, we enrich our analysis with an optimization, called on-the-fly-read-over-write (FlyRow in Table VI), based on read-over-write [66]. This optimization simplifies expressions and resolves load operations ahead of the solver, often avoiding to resort to the duplicated memory and allowing to spare insecurity queries”; Page 1028, “However, inlining all variables is not a viable option as it would lead to an exponential term size growth. Instead, we define a canonical form v + o where v is a bitvector variable, and o is a constant bitvector offset, and we only inline formulas that are in canonical form. It enables rewriting of most of the memory accesses on the stack which are of the form ebp + bv while avoiding term-size explosion”) [Examiner’s remarks: Initial symbolic representation (binary-level relational symbolic execution on expressions) determines if simplification (optimization) can be performed on any memory related operations (load operations).] ; - in case of determining a simplification, generating a simplified symbolic representation of said software instruction to replace the initial symbolic representation (Page 1028, “We define a function untaint(ρ, ȗ, ϕ) that takes a register map ρ, a memory µ, and a duplicated expression ϕ; it applies the rules defined in Fig. 5 which deduce variable equalities from ϕ, propagate them in ρ and ȗ, and return a pair of updated register map and memory (ρ,µ). Intuitively, if the equality of variables vl and vr can be deduced from secLeak(ϕ), the untaint function replaces occurrences of vr by vl in the memory and the register map. As a result, a duplicated expression vl|vr would be replaced by the simple expression vl in the rest of the execution”) [Examiner’s remarks: If a simplification is determined (untaint determining variable equalities) which can be used to generate a simplified symbolic representation (replacing vl|vr with the simple expression vl).] ; and - generating a new symbolic representation of the computer program with the simplified symbolic representation of said software instruction (Page 1028, “We define a function untaint(ρ, ȗ, ϕ) that takes a register map ρ, a memory µ, and a duplicated expression ϕ; it applies the rules defined in Fig. 5 which deduce variable equalities from ϕ, propagate them in ρ and ȗ, and return a pair of updated register map and memory (ρ,µ). Intuitively, if the equality of variables vl and vr can be deduced from secLeak(ϕ), the untaint function replaces occurences of vr by vl in the memory and the register map. As a result, a duplicated expression vl|vr would be replaced by the simple expression vl in the rest of the execution”) [Examiner’s remarks: A new symbolic representation is generated using the simple expression vl instead of vl|vr which is used for the rest of the execution. If the representation is executed in the new form, then it has been updated in the program.] . Regarding claim 5, the rejection of claim 1 is incorporated and Daniel further discloses: - wherein the step of analyzing the initial symbolic representation of a software instruction further comprises a step of reducing the number of memory access (Page 1027, “By keeping track of relational store expressions along the symbolic execution, it can resolve select operations– often avoiding to resort to the duplicated memory– and drastically reduces the number of queries sent to the solver, improving the performances of the analysis.”) [Examiner’s remarks: Queries sent to solver is reduced and duplicated memory is avoided, thereby reducing memory access.] . Regarding claim 10, the rejection of claim 1 is incorporated; and Daniel further discloses: - A system comprising means adapted to carry out the steps of the method according to claim 1 (Page 1029, “Experiments were performed on a laptop with an Intel(R) Core(TM) i5-2520M CPU @ 2.50GHz processor and 32GB of RAM, running Linux Mint 18.3 Sylvia. Similarly to related work (e.g. [23]), esp is initialized to a concrete value, we start the analysis from the beginning of the main function, we statically allocate data structures and the length of keys and buffers is fixed (e.g. for Curve25519-donna [67], three 256-bit buffers are used to store the input, the output and the secret key). When not stated otherwise, programs are compiled for x86 (32bit) with their default compiler setup”) [Examiner’s remarks: The steps of claim one are taught by Daniels and may be executed on a system (computer)] . Regarding claim 11, the rejection of claim 1 is incorporated; and Daniel further discloses: - A computer program comprising instructions for carrying out the steps of the method according to claim 1 when said computer program is executed on a suitable computer device (Page 1029, “Experiments were performed on a laptop with an Intel(R) Core(TM) i5-2520M CPU @ 2.50GHz processor and 32GB of RAM, running Linux Mint 18.3 Sylvia. Similarly to related work (e.g. [23]), esp is initialized to a concrete value, we start the analysis from the beginning of the main function, we statically allocate data structures and the length of keys and buffers is fixed (e.g. for Curve25519-donna [67], three 256-bit buffers are used to store the input, the output and the secret key). When not stated otherwise, programs are compiled for x86 (32bit) with their default compiler setup”) [Examiner’s remarks: Daniels discloses using a computer program (computer) to execute the stated limitations on a suitable computer device (specified computer).] . Claim Rejections - 35 USC § 103 07-06 AIA 15-10-15 In the event the determination of the status of the application as subject to AIA 35 U.S.C. 102 and 103 (or as subject to pre-AIA 35 U.S.C. 102 and 103) is incorrect, any correction of the statutory basis (i.e., changing from AIA to pre-AIA) for the rejection will not be considered a new ground of rejection if the prior art relied upon, and the rationale supporting the rejection, would be the same under either status. 07-20-aia AIA 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. 07-21-aia AIA Claim 2 is rejected under 35 U.S.C. 103 as being unpatentable over “BINSEC/REL: Efficient Relational Symbolic Execution for Constant-Time and Binary Level” by Daniel et. al (hereinafter “Daniel”), in view of “Automatic Equivalence Checking for Assembly Implementations of Cryptography Libraries” by Lim and Nagarakatte (hereinafter “Lim”) . Regarding claim 2, the rejection of claim 1 is incorporated; and Daniel discloses: wherein the step of analyzing an initial symbolic representation of a software instruction comprises: … - else, processing the symbolic expression of the read operation or of the write operation (Page 1026, “LOAD is the evaluation of a load expression. The rule returns a pair of logical select formulas from the pair of symbolic memories µ (the box in the hypotheses should be ignored for now, it will be explained in Section V-A). Note that the returned expression is always duplicated as the select must be performed in the left and right memories independently”; Page 1027, “This optimization simplifies expressions and resolves load operations ahead of the solver, often avoiding to resort to the duplicated memory and allowing to spare insecurity queries”) [Examiner’s remarks: If a symbolic expression is a read or write operation, the expression is processed (optimized).] . Daniel does not explicitly disclose: - determining if the initial symbolic representation of the software instruction comprises a symbolic expression of a read or a write operation; - if not, generating a new symbolic representation of the computer program with the initial symbolic representation of said software instruction; and However, Lim discloses: - determining if the initial symbolic representation of the software instruction comprises a symbolic expression of a read or a write operation (Page 43, “Figure 7(c) presents the equivalent DAG after transforming the memory operations into nested if-then-else nodes. In Figure 7(b), the child of the read operation at index i4 (i.e., T14) is a memory write operation A3 that writes value v3 at index i3. We convert it into an if-then-else node with three children: comparison node (i4=i3), value node v3 for the if part, and nested if-then-else tree for the else part as shown in Figure 7(c). This process is repeated until all the memory write operations are converted into if-then-else nodes”) [Examiner’s remarks: It is determined whether an operation is a read or write operation.] ; - if not, generating a new symbolic representation of the computer program with the initial symbolic representation of said software instruction (Page 43, “Figure 7(c) presents the equivalent DAG after transforming the memory operations into nested if-then-else nodes. In Figure 7(b), the child of the read operation at index i4 (i.e., T14) is a memory write operation A3 that writes value v3 at index i3. We convert it into an if-then-else node with three children: comparison node (i4=i3), value node v3 for the if part, and nested if-then-else tree for the else part as shown in Figure 7(c). This process is repeated until all the memory write operations are converted into if-then-else nodes”) [Examiner’s remarks: The read/write operations are only converted into if-then-else nodes if it is a memory operation. Otherwise, the instruction remains the same.] ; and Therefore, it would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to incorporate the teachings of Lim into the teachings of Daniel to include “determining if the initial symbolic representation of the software instruction comprises a symbolic expression of a read or a write operation” and “if not, generating a new symbolic representation of the computer program with the initial symbolic representation of said software instruction”. As stated in Lim, “Our key idea is to leverage a combination of concrete execution and symbolic evaluation coupled with query decomposition optimizations to reduce the large verification condition into smaller sub-problems domain collaborations [15], arithmetic-aware alias analysis [16,17], to build a very precise taint analysis on C programs” (Page 38). Determining whether an operation is a memory operation allows the program to perform the necessary optimizations for simplifying memory access, while leaving other operations alone allows users to save time during operation by ignoring instructions that do not need to be optimized. Therefore, it would be obvious to one of ordinary skill in the art to combine evaluation of symbolic execution with determination of read/write operations . 07-21-aia AIA Claim s 3-4 are rejected under 35 U.S.C. 103 as being unpatentable over “BINSEC/REL: Efficient Relational Symbolic Execution for Constant-Time and Binary Level” by Daniel et. al (hereinafter “Daniel”), in view of “Verifying Constant-Time Implementations by Abstract Interpretation” by Blazy et. al, (hereinafter “Blazy”) . Regarding claim 3, the rejection of claim 1 is incorporated; and Daniel further discloses: - wherein the analyzing step comprises using context mapping information to determine if a simplification may be applied to the initial symbolic representation of the software instruction, wherein context mapping information is information on previous computations made with variables and memories included in the sequence of software instructions… (Page 1028, “2) Untainting: After the evaluation of a rule with the predicate secLeak for a duplicated expression ϕl|ϕr , we know that the equality ϕl = ϕr holds in the current configuration. From this equality, we can deduce useful information about variables that must be equal in both executions. We can then propagate this information to the register map and memory in order to spare subsequent insecurity queries concerning these variables. For instance, consider the leak of the duplicated expression vl + 1 | vr + 1 , where vl and vr are symbolic variables. If the leak is secure, we can deduce that vl = vr and replace all occurrences of vr by vl in the rest of the symbolic execution”); Page 1028, “We define a function untaint(ρ, ȗ, ϕ) that takes a register map ρ, a memory µ, and a duplicated expression ϕ; it applies the rules defined in Fig. 5 which deduce variable equalities from ϕ, propagate them in ρ and ȗ, and return a pair of updated register map and memory (ρ,µ). Intuitively, if the equality of variables vl and vr can be deduced from secLeak(ϕ), the untaint function replaces occurences of vr by vl in the memory and the register map. As a result, a duplicated expression vl|vr would be replaced by the simple expression vl in the rest of the execution”) [Examiner’s remarks: Daniel discloses a context map (register map) which maps memories and variables used in previous computations, and may be used to simplify an expression by determining if two variables have the same value and thus, may be simplified in subsequent execution.] ; Daniel does not explicitly disclose: - … and information on previous computed abstract domains wherein an abstract domain representing an abstract value attached to a variable or to an expression of the computer program. However, Blazy discloses: - and information on previous computed abstract domains wherein an abstract domain representing an abstract value attached to a variable or to an expression of the computer program Page 2, lines 16-20, “We follow the abstract interpretation methodology: we design an abstract interpreter that executes over security properties instead of concrete values, and use approximation of program executions to perform fix point computations. We hence leverage the inference capabilities of advanced abstract interpretation techniques as relational numeric abstractions [14], abstract domain collaborations [15], arithmetic-aware alias analysis [16,17], to build a very precise taint analysis on C programs”; Page 2 line 46- Page 3 Lines 1-2, “Verasco relies on several abstract domains, including a memory domain that finely tracks properties related to memory contents, taking into account type conversions and pointer arithmetic[17].”; Page 3, lines 13-27, “First, at the bottom of the figure, a large hub of numerical abstract domains is provided to infer numerical invariants on programs. These properties can be relational as for example j+1<= i <= j+2 in a loop (with Octagons or Polyhedra abstract domains). All these domains finely analyze the behavior of machine integers and floating-points (with potential overflows) while unsound analyzers would assume ideal arithmetic. … Second, on top of these numerical abstractions sits an abstract memory functor [17] that tracks fine grained aliases and interacts with the numerical domains. This functor can choose to represent every cell of the same memory block with a single property, or to finely track each specific property of every position in the block. Contrary to many other alias analyses, this approach allows us to reason on local and global variables with the same level of precision, even when the memory addresses are manipulated by the programmer”) [Examiner’s remarks: Blazy discloses tracking abstract domains in order to analyze variables during the taint analysis process. The tracking is based on the original domain used and tracks abstract domains and variables. Daniel discloses using a context mapping to track information during the untainting process. One of ordinary skill in the art understands that the context map used to track information in the taint analysis process of Daniel may be combined with the tracked information in the taint analysis process of Blazy.] . Therefore, it would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to incorporate the teachings of Blazy into the teachings of Daniel to include “and information on previous computed abstract domains wherein an abstract domain representing an abstract value attached to a variable or to an expression of the computer program”. As stated in Blazy, “We follow the abstract interpretation methodology: we design an abstract interpreter that executes over security properties instead of concrete values, and use approximation of program execution stoper to perform fix point computations. We hence leverage the inference capabilities of advanced abstract interpretation techniques as relational numeric abstractions [14], abstract domain collaborations [15], arithmetic-aware alias analysis [16,17], to build a very precise taint analysis on C programs” (Page 2, lines 16-20). Using and updating abstract domains for code analysis allows for more precise analysis that is also general enough to cover multiple possibilities without introducing too many false positives. Therefore, it would be obvious to one of ordinary skill in the art to combine context mapping with tracking of relevant abstract domains. Regarding claim 4, the rejection of claim 3 is incorporated; and Daniel does not explicitly disclose: - further comprising a step of updating abstract domains of the context mapping according to abstract domains of the initial symbolic representation of the software instruction. However, Blazy discloses: - further comprising a step of updating abstract domains of the context mapping according to abstract domains of the initial symbolic representation of the software instruction (Page 3, lines 13-32, “First, at the bottom of the figure, a large hub of numerical abstract domains is provided to infer numerical invariants on programs. These properties can be relational as for example j+1<= i <= j+2 in a loop (with Octagons or Polyhedra abstract domains). All these domains finely analyze the behavior of machine integers and floating-points (with potential overflows) while unsound analyzers would assume ideal arithmetic. They are connected all-together via communication channels that allow each domain to improve its own precision via specific queries to other domains. As a consequence, Verasco is able to infer subtle numerical invariants that require complex reasoning about linear arithmetic, congruence and symbolic equalities. Second, on top of these numerical abstractions sits an abstract memory functor [17] that tracks fine grained aliases and interacts with the numerical domains. This functor can choose to represent every cell of the same memory block with a single property, or to finely track each specific property of every position in the block. Contrary to many other alias analyses, this approach allows us to reason on local and global variables with the same level of precision, even when the memory addresses are manipulated by the programmer. Some unavoidable approximations are performed when the target of a memory dereference corresponds to several possible targets, but Verasco makes the impact of such imprecision as limited as possible. Because of ubiquitous pointer arithmetic in C programs (even simple array accesses are represented via pointer arithmetic in C semantics), the functor needs to ask advanced symbolic numerical queries to the abstract numerical domain below it. In return, its role is to hide from them the load and store operations, and only communicate via symbolic numerical variables”) [Examiner’s remarks: Blazy discloses tracking abstract domains in order to analyze variables during the taint analysis process. The tracking is based on the original domain used and is tracked as the block is analyzed, thereby updating. Daniel discloses using a context mapping to track information during the untainting process. One of ordinary skill in the art understands that the context map used to track information in the taint analysis process of Daniel may be combined with the tracked information in the taint analysis process of Blazy.] . Therefore, it would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to incorporate the teachings of Blazy into the teachings of Daniel to include “further comprising a step of updating abstract domains of the context mapping according to abstract domains of the initial symbolic representation of the software instruction”. As stated in Blazy, “We follow the abstract interpretation methodology: we design an abstract interpreter that executes over security properties instead of concrete values, and use approximation of program execution stoper to perform fix point computations. We hence leverage the inference capabilities of advanced abstract interpretation techniques as relational numeric abstractions [14], abstract domain collaborations [15], arithmetic-aware alias analysis [16,17], to build a very precise taint analysis on C programs” (Page 2, lines 16-20). Using and updating abstract domains for code analysis allows for more precise analysis that is also general enough to cover multiple possibilities without introducing too many false positives. Therefore, it would be obvious to one of ordinary skill in the art to combine context mapping with updates of context mapping during analysis . 07-21-aia AIA Claim s 8-9 are rejected under 35 U.S.C. 103 as being unpatentable over “BINSEC/REL: Efficient Relational Symbolic Execution for Constant-Time and Binary Level” by Daniel et. al (hereinafter “Daniel”), in view of “Memory Instructions: Load and Store” by Azeria (hereinafter “Azeria”) . Regarding claim 8, the rejection of claim 1 is incorporated; and Daniel discloses: - wherein the step of reducing the number of memory access comprises the steps of … and that the current context mapping contains an expression for the memory M' defined in the received instruction, to generate a simplified symbolic representation of said software instruction to replace the initial symbolic representation ((Page 1028, “2) Untainting: After the evaluation of a rule with the predicate secLeak for a duplicated expression ϕl|ϕr , we know that the equality ϕl = ϕr holds in the current configuration. From this equality, we can deduce useful information about variables that must be equal in both executions. We can then propagate this information to the register map and memory in order to spare subsequent insecurity queries concerning these variables. For instance, consider the leak of the duplicated expression vl + 1 | vr + 1 , where vl and vr are symbolic variables. If the leak is secure, we can deduce that vl = vr and replace all occurrences of vr by vl in the rest of the symbolic execution”) [Examiner’s remark: A value of M can be determined to be the same and therefore replaced in the symbolic representation.] ) . Daniel does not explicitly disclose: - determining that the received instruction is in the form “ X: = load (M’, a’)” of a load of a value a' to a memory M', However, Azeria discloses: - determining that the received instruction is in the form “ X: = load (M’, a’)” of a load of a value a' to a memory M' (See Screenshot from page 2 of Azeria attached below, under “This is how it would look like in a functional assembly program”.) [Examiner’s remarks: Azeria shows load instructions “ldr” which include r1 which is the memory M’ and adr_var1 which is the name of value a’.] … PNG media_image1.png 167 710 media_image1.png Greyscale Therefore, it would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to incorporate the teachings of Azeria into the teachings of Daniel to include “determining that the received instruction is in the form “ X: = load (M’, a’)” of a load of a value a' to a memory M'”. As stated in Azeria, “LDR operation: loads the value at the address found in R0 to the destination register R2… This is how it would look like in a functional assembly program” (Page 1). Defining load instructions in terms of memory location and value is well known in the art and commonly used in assembly. Therefore, it would be obvious to one of ordinary skill in the art to combine simplification of code with loads specifying memory address and variable name. Regarding claim 9, the rejection of claim 8 is incorporated; and Daniel further discloses: - further comprising before generating a simplified symbolic representation of said software instruction, a step of determining if the value a' in the load instruction is equal to a value a defined in the expression of the current context mapping (Page 1028, “We define a function untaint(ρ, ȗ, ϕ) that takes a register map ρ, a memory µ, and a duplicated expression ϕ; it applies the rules defined in Fig. 5 which deduce variable equalities from ϕ, propagate them in ρ and ȗ, and return a pair of updated register map and memory (ρ,µ). Intuitively, if the equality of variables vl and vr can be deduced from secLeak(ϕ), the untaint function replaces occurences of vr by vl in the memory and the register map. As a result, a duplicated expression vl|vr would be replaced by the simple expression vl in the rest of the execution”) [Examiner’s remarks: A value (vl and vr) may be determined to be equal based on the current context mapping (register map), and then subsequently used to update the expression for the rest of execution.] . Allowable Subject Matter 07-43-02 Claims 6-7 would be allowable if rewritten to overcome the rejection(s) under 35 U.S.C. 101, set forth in this Office action and to include all of the limitations of the base claim and any intervening claims. Pertinent Prior Art 07-96 AIA The prior art made of record and not relied upon is considered pertinent to applicant's disclosure. - US 6286135 B1 discloses a method for processing memory in virtual address space . - “Fine-grain Memory Object Representation in Symbolic Execution” by Nowack discloses reducing memory operations in symbolic execution. Conclusion Any inquiry concerning this communication or earlier communications from the examiner should be directed to VIVIAN WEIJIA DUAN whose telephone number is (703)756-5442. The examiner can normally be reached Monday-Friday 8:30AM-5PM. 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, Wei Y Mui can be reached at (571) 272-3708. 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. /V.W.D./Examiner, Art Unit 2191 /WEI Y MUI/Supervisory Patent Examiner, Art Unit 2191 Application/Control Number: 18/722,874 Page 2 Art Unit: 2191 Application/Control Number: 18/722,874 Page 3 Art Unit: 2191 Application/Control Number: 18/722,874 Page 4 Art Unit: 2191 Application/Control Number: 18/722,874 Page 5 Art Unit: 2191 Application/Control Number: 18/722,874 Page 6 Art Unit: 2191 Application/Control Number: 18/722,874 Page 7 Art Unit: 2191 Application/Control Number: 18/722,874 Page 8 Art Unit: 2191 Application/Control Number: 18/722,874 Page 9 Art Unit: 2191 Application/Control Number: 18/722,874 Page 10 Art Unit: 2191 Application/Control Number: 18/722,874 Page 11 Art Unit: 2191 Application/Control Number: 18/722,874 Page 12 Art Unit: 2191 Application/Control Number: 18/722,874 Page 13 Art Unit: 2191 Application/Control Number: 18/722,874 Page 14 Art Unit: 2191 Application/Control Number: 18/722,874 Page 15 Art Unit: 2191 Application/Control Number: 18/722,874 Page 16 Art Unit: 2191 Application/Control Number: 18/722,874 Page 17 Art Unit: 2191 Application/Control Number: 18/722,874 Page 18 Art Unit: 2191 Application/Control Number: 18/722,874 Page 19 Art Unit: 2191 Application/Control Number: 18/722,874 Page 20 Art Unit: 2191 Application/Control Number: 18/722,874 Page 21 Art Unit: 2191 Application/Control Number: 18/722,874 Page 22 Art Unit: 2191 Application/Control Number: 18/722,874 Page 23 Art Unit: 2191
Prosecution Insights