DETAILED ACTION
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 .
Claims 1-9 are presented for examination.
Priority
The claim for priority from US Provisional 63/521,667 filed on 17 June 2023 is duly noted.
Claim Rejections - 35 USC § 102
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.
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 –
Claim(s) 1, 3, 4, 6, 7, and 9 is/are rejected under 35 U.S.C. 102(a)(1) as being anticipated by Hawblitzel et al. (US Patent 9,536,093 B2 and Hawblitzel hereinafter).
As to claims 1, 4, and 7, Hawblitzel discloses a system and method for automated verification of a software system, the system and method having:
memory (col. 20, lines 25-28);
at least one hardware processor collectively configured to at least (col. 20, lines 25-28):
identify a plurality of layers of code of the software including a lowest layer, a middle layer, and a highest layer (112, 116, 120, Figure 1);
generate a low-level (high) specification and an identical refinement proof for each of the plurality of layers (col. 3, lines 26-37);
generate a high-level (low) specification and a lifting refinement proof for each of the plurality of layers (col. 3, lines 26-37);
verify the software based on the low-level specifications, the identical refinement proofs, the high-level specifications, and the lifting refinement proofs (Abstract, lines 7-9; col. 3, lines 33-47).
As to claims 3, 6, and 9, Hawblitzel discloses:
wherein one of the high-level specifications is generated by applying a set of transformation rules to one of the low-level specifications (Abstract, lines 5-7; col. 3, lines 30-33).
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.
This application currently names joint inventors. In considering patentability of the claims the examiner presumes that the subject matter of the various claims was commonly owned as of the effective filing date of the claimed invention(s) absent any evidence to the contrary. Applicant is advised of the obligation under 37 CFR 1.56 to point out the inventor and effective filing dates of each claim that was not commonly owned as of the effective filing date of the later invention in order for the examiner to consider the applicability of 35 U.S.C. 102(b)(2)(C) for any potential 35 U.S.C. 102(a)(2) prior art against the later invention.
Claim(s) 2, 5, and 8 is/are rejected under 35 U.S.C. 103 as being unpatentable over Hawblitzel as applied to claims 1, 4, and 7 above, and further in view of Chang et al. (US Patent 11,868,481 B2 and Chang hereinafter).
As to claims 2, 5, and 8, Hawblitzel fails to specifically disclose:
wherein one of the low-level specifications is generated using Fixedpoint construction.
Nonetheless, this feature is well known in the art and would have been an obvious modification of the teachings disclosed by Hawblitzel, as taught by Chang.
Chang discloses a system and method for discovering vulnerabilities of operating system access control mechanism based on model checking, the system and method having:
wherein one of the low-level specifications is generated using Fixedpoint construction (col. 1, line 64-col. 2, line 2).
Given the teaching of Chang, a person having ordinary skill in the art before the effective filing date of the claimed invention would have readily recognized the desirability and advantages of modifying the teachings of Hawblitzel with the teachings of Chang by using Fixed-point construction. Chang recites motivation by disclosing that using fixed point construction allows for the checking for violations and thus increased security (col. 1, line 57-col. 2, line 6). It is obvious that the teachings of Chang would have improved the teachings of Hawblitzel by using fixed-point construction in order to allow for the checking of violations and increasing security.
Prior Art Made of Record
The prior art made of record and not relied upon is considered pertinent to applicant's disclosure.
Boulton (WO 2019/034559 A1) discloses a system and method for generating security manifests for software components using binary static analysis.
Danielson et al. (US 2022/0318127 A1) discloses a system and method for software compiler integrity verification.
Jaouen et al. (US 2023/0040093 A1) discloses a system and method for verifying an execution of a software program.
Niu et al. (CN 116244702 A) discloses a system and method for Android software static analysis based on mixed mode.
Shao et al. (US 2020/0387440 A1) discloses a system and method for formal verification.
Yao (WO 2010/105249 A1) discloses a system and method for detection of malware.
Zhan et al. (CN 113946831 A) discloses a system and method for cross-platform new software based on micro-service and new system safety risk analysis.
Conclusion
Any inquiry concerning this communication or earlier communications from the examiner should be directed to SARAH SU whose telephone number is (571)270-3835. The examiner can normally be reached 6:30 AM - 3:00 PM.
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, Lynn Feild can be reached at 571-272-2092. 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.
/SARAH SU/Primary Examiner, Art Unit 2431