WO2025017925A1 - Proof verification system and proof verification method - Google Patents

Abstract

The present disclosure is a proof verification system comprising: a proof terminal that proves the safety of a high-level language program; and a verification terminal that verifies the safety of the program. The proof terminal comprises: a compiler that generates an executable file on the basis of a source code of the program; a logical expression generation unit that generates an intermediate representation on the basis of the source code of the program, and generates, on the basis of secret definition information indicating that a prescribed variable name in the intermediate representation and in the high-level language is confidential information, a verification logical expression indicating a condition to be established immediately before and immediately after executing the executable file of the program; a proof creation unit that demonstrates that the executable file satisfies the condition on the basis of the verification logical expression, and creates a safety proof for guaranteeing the safety of the executable file; and an output unit that outputs the executable file, the verification logical expression, and the safety proof.

Description

Proof verification system and proof verification method

This disclosure relates to a proof verification system and a proof verification method.

The widespread use of open technologies has led to an increase in standardization and diversification of software components, even in critical systems. In recent years, cyber attacks targeting the software supply chain have also become evident.

The use of Proof-Carrying Code (PCC) has been proposed as a conventional technique for ensuring that software is safe (Non-Patent Document 1). PCC is a technique that makes it possible to guarantee the authenticity of a program and prove that the program meets desired safety requirements by distributing a proof of the program's safety along with the program. In conventional techniques, this allows users of the program to verify that confidential information such as passwords is stored safely by analyzing the program (software) and expressing the safety requirements, such as that confidential information such as passwords is hashed and stored in the correct procedure, in the form of a verification logical formula.

Tokoshi Tsubasa, Yoshimura Hitoshi, Nakabayashi Misato, Okuda Tetsuya, "A method of securely executing programs using Proof-Carrying Code and TEE", Computer Security Research Report (CSEC), 2022-CSEC-97, 2022-05-12

However, conventional technology only analyzes specific high-level languages such as C++. When multiple languages are used in the software supply chain, analysis is required for each language, which increases the effort required to perform formal verification of the program.

The present invention was made in consideration of the above points, and aims to reduce the amount of work required to verify a program.

　In order to achieve the above object, the invention according to claim 1 is a proof verification system having a proof terminal that proves the safety of a program in a high-level language and a verification terminal that verifies the safety of the program, the proof terminal having a compiler that generates an executable file based on the source code of the program, a logical expression generation unit that generates an intermediate representation based on the source code of the program, and generates a verification logical expression indicating a condition that should be satisfied immediately before and after the executable file of the program is executed based on the intermediate representation and confidential definition information indicating confidentiality indicating that a specific variable name in the high-level language is confidential information, a proof creation unit that creates a safety proof to prove that the executable file satisfies the condition based on the verification logical expression and ensure the safety of the executable file, and an output unit that outputs the executable file, the verification logical expression, and the safety proof, and the verification terminal has a proof confirmation unit that confirms that the safety proof obtained from the proof terminal exists if the executable file satisfies the condition based on the verification logical expression.

As described above, the present invention has the effect of reducing the amount of work required to verify a program.

1 is a schematic diagram of a proof verification system according to a first embodiment. FIG. 2 is a diagram illustrating the electrical hardware configuration of each terminal. FIG. 2 is a functional configuration diagram of a certification terminal according to the first embodiment; FIG. 2 is a functional configuration diagram of a verification terminal according to the first embodiment. 2 is a sequence diagram showing the processing or operation of the proof verification system according to the first embodiment. FIG. 4 is a flowchart showing a process or operation of a verification terminal which is a premise of the first embodiment; FIG. 11 is a functional configuration diagram of a certification terminal according to the second embodiment. FIG. 11 is a sequence diagram showing the processing or operation of the proof verification system according to the second embodiment. FIG. 13 is a functional configuration diagram of a certification terminal according to the third embodiment. FIG. 13 is a sequence diagram showing the processing or operation of the proof verification system according to the third embodiment.

Each embodiment of the present invention will be described below. In this embodiment, the processing or operation of a program developer and user in a series of distribution processes in the software supply chain (design, development, and manufacturing of equipment and software, function addition, introduction, and operation (or use)) will be described.

First Embodiment First, the first embodiment will be described.

[Overall configuration]
Fig. 1 is a schematic diagram of a proof verification system according to the first embodiment. As shown in Fig. 1, the proof verification system 10 of the first embodiment is constructed by a proof terminal 30 and a verification terminal 50. In this case, the proof terminal 30 is a terminal that proves the safety of a program and creates a safety proof p, etc., and in this embodiment, it is also a development terminal of a program developer. The verification terminal 50 is a terminal that verifies the safety of a program and in this embodiment, it is also a user terminal of a program user. The verification terminal 50 executes a program (executable file) after confirming the existence of the safety proof p.

[Electrical configuration of each terminal]
Next, the electrical hardware configuration of each terminal will be described with reference to Fig. 2. Fig. 2 is a diagram showing the electrical hardware configuration of each terminal.

As shown in FIG. 2, each terminal (certification terminal 30, verification terminal 50) is a computer that includes a CPU 101, a ROM 102, a RAM 103, an SSD 104, an external device connection I/F (Interface) 105, a network I/F 106, a display device 107, an input device 108, a media I/F 109, and a bus line 110.

Of these, CPU 101 controls the overall operation of each terminal. ROM 102 stores programs used to drive CPU 101, such as IPL. RAM 103 is used as a work area for CPU 101.

The SSD 104 reads and writes various data according to the control of the CPU 101. Note that a HDD (Hard Disk Drive) may be used instead of the SSD 104.

The external device connection I/F 105 is an interface for connecting various external devices. In this case, the external devices include a display, a speaker, a keyboard, a mouse, a USB memory, and a printer.

The network I/F 106 is an interface for data communication via a communication network such as the Internet.

The display device 107 is a type of display means, such as a liquid crystal or organic EL (Electro Luminescence) device, that displays various images. An example of the display device 107 is a display.

The input device 108 is a type of input means for selecting and executing various instructions, selecting a processing target, moving a cursor, etc. An example of the input device 108 is a pointing device.

The media I/F 109 controls the reading and writing (storing) of data from and to a recording medium 109m such as a flash memory. Recording media 109m includes DVDs and Blu-ray Discs (registered trademarks).

The bus line 110 is an address bus, a data bus, etc., for electrically connecting each component such as the CPU 101 shown in FIG. 2.

[Functional configuration of the proof verification system according to the first embodiment]
Next, the functional configuration of each terminal (the certification terminal 30a, the verification terminal 50) of the proof verification system 10 according to the first embodiment will be described with reference to FIG. 3 and FIG.

<Certification terminal>
3 is a functional configuration diagram of the certification terminal according to the first embodiment. Note that the certification terminal 30a is an example of the certification terminal 30 shown in FIG.

As shown in FIG. 3, the proof terminal 30a has an acquisition unit 31, a compiler 32, a logical formula generation unit 35a, a proof creation unit 36, and an output unit 39. Each of these units is a function that the CPU 101 as a processor causes the proof terminal 30a to realize using one or more programs installed in the proof terminal 30a.

The acquisition unit 31 acquires source code s written in a programming language through the operation of the prover (developer).

The compiler 32 is a general compiler that reads and analyzes the source code s and converts (generates) it into an executable file (binary) b that can be directly executed by the computer.

The logical formula generation unit 35a generates a verification logical formula v based on confidential definition information c that is set in advance by the developer and the source code s acquired from the acquisition unit 31. The developer also creates confidential definition information while creating a program in a high-level language, and indicates confidential parts in the confidential definition information. The "confidential definition information" indicates that a specific variable name in the high-level language (e.g., "password") is confidential information.

An example of a method for generating the verification logical formula v is disclosed in Reference 1.
(Reference 1) Proof-of-concealment in interactive program distribution with proven security and its applications, Yasuaki Tsukada, 2005
Verification formula v is a condition (pre-condition, post-condition) that must be satisfied immediately before and after the execution of a program (executable file b), and is provided in advance by the user of the program to the developer. If verification formula v is a valid formula, it is mathematically guaranteed that "when executable file b is executed in a situation where the pre-condition is satisfied and the calculation is completed, the post-condition will always be satisfied, and the safety required by the user will be met when executable file b is executed."

The logical formula generation unit in Reference 1 has both the front-end functionality (the functionality of parsing source code s) and the back-end functionality (the functionality of creating an executable file) of the compiler in order to generate the verification logical formula v.

In contrast, the logical formula generation unit 35a of this embodiment does not have a back-end function, or if it has a back-end function, it does not execute it, but has a front-end function. As a result, the logical formula generation unit 35a generates up to an intermediate representation (LLVM-IR) during the compilation process, and generates a verification logical formula v using this intermediate representation. As a result, by sending the verification logical formula v using the intermediate representation (LLVM-IR) common to each language to the verification terminal 50 in the subsequent process, even if multiple languages are used in the software supply chain, there is no need to perform analysis corresponding to each language, and the labor required for formal verification of the program can be reduced.

The proof creation unit 36, as shown in the above-mentioned reference 1, verifies that the executable file b satisfies the pre-condition and post-condition based on the verification logical formula v, and creates a safety proof p to guarantee the safety of the executable file b.

The output unit 39 obtains the executable file b from the compiler 32, the security proof p from the proof creation unit 36, and the verification logical formula v from the logical formula generation unit 35, and outputs all of this data. Each output data may be transmitted to the verification terminal 50 via a communication network such as the Internet, or may be recorded on a recording medium such as a DVD-ROM and sent to the verification terminal 50.

<Verification terminal>
FIG. 4 is a functional configuration diagram of the certification terminal according to the first embodiment.

As shown in FIG. 4, the verification terminal 50 has an acquisition unit 51, a proof verification unit 56, and an execution unit 59. Each of these units is a function that the CPU 101 as a processor realizes in the verification terminal 50 using one or more programs installed in the verification terminal 50.

The acquisition unit 51 acquires the above data output from the certification terminal 30 through the operation of the verifier (user).

The proof confirmation unit 56 confirms the existence of the safety proof p. In this case, the proof confirmation unit 56 confirms the existence of the safety proof p by performing the same processing as the proof creation unit 36 using each of the above data. Specifically, the proof confirmation unit 56 uses each of the above data to determine whether the executable file b satisfies the above conditions (pre-condition and post-condition) based on the verification logical formula v, just like the proof creation unit 36, and if it does, confirms that the safety proof p obtained from the certification terminal 30 certainly exists.

If the proof checking unit 56 confirms the existence of the security proof p, the execution unit 59 executes the executable file b acquired from the acquisition unit 51.

[Processing or Operation of the First Embodiment]
Next, the processing or operation of the first embodiment will be described with reference to Fig. 5 and Fig. 6. Fig. 5 is a sequence diagram showing the processing or operation of the proof verification system according to the first embodiment. Fig. 6 is a flowchart showing the processing or operation of the verification terminal according to the first embodiment.

S131: The acquisition unit 31 acquires source code s written in a programming language through the operation of the prover (developer).

S132: The compiler 32 reads the source code s and generates an executable file (binary) b.

S133: The logical expression generation unit 35a generates an intermediate representation r based on the source code s acquired from the acquisition unit 31.

S134: The logical formula generation unit 35a generates a verification logical formula v based on the intermediate representation r and the confidential definition information c.

S135: The proof creation unit 36 verifies that the executable file b satisfies the pre-condition and post-condition based on the verification logical formula v, and creates a safety proof p to guarantee the safety of the executable file b.

S136: The output unit 39 obtains the executable file b from the compiler 32, obtains the security proof p from the proof creation unit 36, and obtains the verification logical formula v from the logical formula generation unit 35, and transmits each data to the verification terminal 50. As a result, the acquisition unit 51 of the verification terminal 50 acquires each data.

S151: Proceeding to FIG. 6, the verification terminal 50's proof checking unit 56 uses the above data to perform processing similar to that of the proof creation unit 36, thereby confirming the existence of the security proof p.

S152: If the proof checking unit 56 is able to confirm the existence of the safety proof p (S151; True), the execution unit 59 executes the executable file. On the other hand, if the proof checking unit 56 is unable to confirm the existence of the safety proof p (S151; False), the safety of the executable file cannot be guaranteed, so the execution unit 59 does not execute the executable file, and the process shown in FIG. 6 ends.

[Major Effects of the First Embodiment]
As described above, according to this embodiment, the certification terminal 30a sends the verification logical formula v using an intermediate representation (LLVM-IR) common to each language to the downstream verification terminal 50. This eliminates the need for analysis corresponding to each language, even when multiple languages are used in the software supply chain, and makes it possible to reduce the labor required for formal verification of a program.

Second embodiment Next, a second embodiment will be described with reference to Fig. 7 and Fig. 8. The second embodiment also has the overall configuration as shown in Fig. 1. The certification terminal 30b is an example of the certification terminal 30 shown in Fig. 1.

First, an overview of the differences from the first embodiment will be explained. In the first embodiment, if source code s in a high-level language contains confidential information in the name of a variable such as "password", the intermediate representation generated from the source code s is difficult for humans to read, making it difficult for a verifier in a later process to confirm which part of the executable file b is confidential information. To solve this problem, the second embodiment generates the variable name in the intermediate representation (the number from the beginning, such as "20") and a label indicating that the variable name is confidential information. A detailed explanation is provided below.

[Functional configuration of the proof verification system according to the second embodiment]
The functional configuration of the proof terminal 30b of the proof verification system 10 according to the second embodiment will be described with reference to FIG.

<Certification terminal>
Fig. 7 is a functional configuration diagram of a certification terminal according to the second embodiment. As shown in Fig. 7, the certification terminal 30b has an acquisition unit 31, a compiler 32, a labeling information generation unit 34b, a logical formula generation unit 35b, a proof creation unit 36, and an output unit 39. These units are functions that the CPU 101 as a processor realizes in the certification terminal 30b using one or more programs installed in the certification terminal 30b. Note that, here, the same reference numerals are used to designate the same functional configurations of the first embodiment shown in Fig. 3, and the description thereof will be omitted.

The labeling information generation unit 34b, like the logical formula generation units 35a and 35b, has the function of generating an intermediate representation (LLVM-IR). Based on confidential definition information c indicating that a variable name (e.g., "password") in a high-level language is confidential information, the labeling information generation unit 34b analyzes the source code s acquired from the acquisition unit 31, and generates auxiliary information a, which is an intermediate representation that inherits attribute information in the high-level language (variable name (e.g., "password"), function name, and program file name).

The labeling information generation unit 34b also generates labeling information L2 based on the auxiliary information a. The labeling information generation unit 34b uses a predetermined tool that associates a predetermined variable name in the high-level language (e.g., "password") with the order of the variables from the beginning in the intermediate representation r (e.g., "20"). This allows the labeling information generation unit 34b to generate labeling information that is a pair of the variable name "20th" and a label indicating that this is confidential information, using auxiliary information a indicating that the variable name "password" is confidential information and a predetermined tool indicating that the variable name "password" is variable name "20th".

The "labeling information" includes a pair of a specific variable name in the intermediate representation r and a label to be assigned to this specific variable. The "label" indicates that the part of the specific variable name is confidential information.

The logical expression generation unit 35b, like the logical expression generation unit 35a, generates an intermediate representation r based on the source code s acquired from the acquisition unit 31.

The logical formula generation unit 35b generates a verification logical formula v based on the generated intermediate representation r and the labeling information L2 (a set of a variable name (e.g., "20") and a label (e.g., "confidential information")) generated by the labeling information generation unit 34b. The method of generating the verification logical formula v is the same as in the first embodiment.

[Processing or Operation of the Second Embodiment]
Next, the process or operation of the second embodiment will be described with reference to Fig. 8. Fig. 8 is a sequence diagram showing the process or operation of the proof verification system according to the second embodiment. Note that the process or operation of the verification terminal 50 according to the second embodiment is the same as that of the first embodiment, and therefore the description thereof will be omitted.

S231: The acquisition unit 31 acquires source code s written in a programming language through the operation of the prover (developer).

S232: The compiler 32 reads the source code s and generates an executable file (binary) b.

S233: The logical expression generation unit 35b generates an intermediate representation r based on the source code s acquired from the acquisition unit 31.

S234: The labeling information generating unit 34b analyzes the source code s acquired from the acquiring unit 31 based on the confidential definition information c, and generates auxiliary information a, which is an intermediate representation that inherits the attribute information in the high-level language.

S235: The labeling information generation unit 34b generates labeling information L2 based on the auxiliary information a.

S236: The logical formula generation unit 35b generates a verification logical formula v based on the intermediate representation r and the labeling information L2.

S237: The proof creation unit 36 verifies that the executable file b satisfies the pre-condition and post-condition based on the verification logical formula v, and creates a safety proof p to guarantee the safety of the executable file b.

S238: The output unit 39 obtains the executable file b from the compiler 32, obtains the security proof p from the proof creation unit 36, and obtains the verification logical formula v from the logical formula generation unit 35, and transmits each data to the verification terminal 50. As a result, the acquisition unit 51 of the verification terminal 50 obtains each data.

[Major Effects of the Second Embodiment]
As described above, according to this embodiment, in addition to the effects of the first embodiment, variable names in the intermediate representation r (such as the sequence "20" from the beginning) and labels indicating that the variable names are confidential information are generated. This has the effect that even if confidential information in the variable names such as "password" is included in the source code s in a high-level language, a verifier in a later process can easily confirm which part of the executable file b is confidential information.

Third embodiment Next, a third embodiment will be described with reference to Fig. 9 and Fig. 10. The third embodiment also has the overall configuration as shown in Fig. 1. The certification terminal 30c is an example of the certification terminal 30 shown in Fig. 1.

The third embodiment assumes processing or operations performed in an open source supply chain using GitHub or the like. Git is a distributed version control system, and is a tool used by developers. GitHub is a web service that uses the Git mechanism to enable people all over the world to store and publish their own work (program code, design data, etc.). The third embodiment assumes a situation in which, for example, in an open source supply chain, developer B replicates a program developed by developer A and adds a new program.

First, an outline of the differences from the second embodiment will be explained. In the second embodiment, if a developer makes a small modification or alteration to a program published on GitHub or the like, regenerating all of the verification logical formulas v will take time or will result in the generation of duplicated verification logical formulas v. This reduces the efficiency of the work of the developer and verifier. In the third embodiment, to solve this problem, a new verification logical formula v is generated without changing the duplicated parts (common parts) of the verification logical formula v before and after the modification or alteration. For example, if the verification logical formula v2 after the modification or alteration completely contains the verification logical formula v1 after the modification or alteration, only the verification logical formula v2 is left, without leaving both the verification logical formula v1 and the verification logical formula v2. This will be explained in detail below.

[Functional configuration of the proof verification system according to the third embodiment]
The functional configuration of the proof terminal 30c of the proof verification system 10 according to the third embodiment will be described with reference to FIG.

<Certification terminal>
9 is a functional configuration diagram of the proof terminal according to the third embodiment. As shown in FIG. 9, the proof terminal 30b has an acquisition unit 31, a compiler 32, a labeling information generation unit 34c, a logical expression generation unit 35c, a proof creation unit 36, and an output unit 39. These units are functions that the CPU 101 as a processor realizes in the proof terminal 30c using one or more programs installed in the proof terminal 30c. Here, among the functional configurations of the first and second embodiments shown in FIG. 7, the same reference numerals are used for the similar functional configurations, and the description thereof is omitted. Note that the labeling information generation unit 34c and the logical expression generation unit 35c are modified versions of the labeling information generation unit 34b and the logical expression generation unit 35b in the second embodiment, respectively.

The labeling information generating unit 34c basically includes the same functions as the labeling information generating unit 34b, and further combines the auxiliary information a1 acquired from another terminal and the auxiliary information a2 generated by its own terminal (the certification terminal 30c) into one file, and generates the labeling information L3 based on the combined auxiliary information a1 and a2. The auxiliary information a1 is information acquired from GitHub or the like by the acquisition unit 31, and is an example of the auxiliary information a by another developer A. The auxiliary information a2 is an example of the auxiliary information a generated by the labeling information generating unit 34c in the certification terminal 30c of developer B in the same procedure as the labeling information generating unit 34b. Each piece of auxiliary information a1 and a2 includes attribute information (variable name (e.g., "password"), function name, and program file name), so the labeling information generating unit 34c combines the auxiliary information a1 and the auxiliary information a2 based on the attribute information of each piece of auxiliary information a1 and a2.

The logical formula generation unit 35c basically includes the same functions as the logical formula generation unit 35b, and further combines the intermediate representation r1 acquired from another terminal and the intermediate representation r2 generated on its own terminal (the proof terminal 30c) into one file. The intermediate representation r1 is information acquired from GitHub or the like by the acquisition unit 31, and is an example of an intermediate representation r by another developer A. The intermediate representation r2 is an example of an intermediate representation r generated by the logical formula generation unit 35c in the proof terminal 30c of developer B in the same procedure as the logical formula generation unit 35b. Each intermediate representation r1, r2 includes attribute information (variable name (e.g., "20"), function name, and program file name), so the labeling information generation unit 34c combines the intermediate representation r1 and the intermediate representation r2 based on the attribute information of each intermediate representation r1, r2.

The logical formula generation unit 35c generates a verification logical formula v based on the combined intermediate representations r1 and r2 and the labeling information L3 (a set of variable names (e.g., "20") and labels (e.g., "confidential information")) generated by the labeling information generation unit 34c. Note that in this case, due to program modification or alteration, more sets of variable names and labels may be generated than in the second embodiment.

[Processing or Operation of the Third Embodiment]
Next, the processing or operation of the third embodiment will be described with reference to FIG. 10. FIG. 10 is a sequence diagram showing the processing or operation of the proof verification system according to the third embodiment. The processing or operation of the verification terminal 50 according to the third embodiment is similar to that of the first embodiment, and therefore the description will be omitted. Furthermore, the intermediate representation r1 is an example of the first intermediate representation, and the intermediate representation r2 is an example of the second intermediate representation. The auxiliary information a1 is an example of the first auxiliary information, and the auxiliary information a2 is an example of the second auxiliary information. Furthermore, the secret definition information used in the other certification terminals is an example of the first secret definition information, and the secret definition information used in the certification terminal 30c is an example of the second secret definition information.

S331: The acquisition unit 31 acquires source code s written in a programming language through the operation of the prover (developer).

S332: The compiler 32 reads the source code s and generates an executable file (binary) b.

S333: The acquisition unit 31 acquires the intermediate representation r1 and auxiliary information a1 generated by another certification terminal from GitHub or the like in the open source supply chain. The intermediate representation r1 and auxiliary information a1 correspond to the intermediate representation r and auxiliary information a in the second embodiment, respectively.

S334: The logical expression generation unit 35c generates an intermediate representation r2 based on the source code s acquired from the acquisition unit 31.

S335: The logical formula generation unit 35c combines the intermediate representation r1 acquired from the acquisition unit 31 and the intermediate representation r2 generated by the logical formula generation unit 35c into one file.

S336: The labeling information generation unit 34c analyzes the source code s acquired from the acquisition unit 31 based on the confidential definition information c2 created by the developer using the certification terminal 30c, and generates auxiliary information a2, which is an intermediate representation r2 that inherits the attribute information in the high-level language.

S337: The labeling information generation unit 34c combines the auxiliary information a1 acquired from the acquisition unit 31 and the auxiliary information a2 generated by the labeling information generation unit 34c into one file.

S338: The labeling information generation unit 34c generates labeling information L3 based on the combined auxiliary information a1 and a2.

S339: The logical formula generation unit 35c generates a verification logical formula v based on the combined intermediate representations r1 and r2 and the labeling information L3.

S340: The proof creation unit 36 verifies that the executable file b satisfies the pre-condition and post-condition based on the verification logical formula v, and creates a safety proof p to guarantee the safety of the executable file b.

S341: The output unit 39 obtains the executable file b from the compiler 32, obtains the security proof p from the proof creation unit 36, and obtains the verification logical formula v from the logical formula generation unit 35, and transmits each data to the verification terminal 50. As a result, the acquisition unit 51 of the verification terminal 50 acquires each data.

[Major Effects of the Third Embodiment]
As described above, according to this embodiment, in addition to the effects of the first and second embodiments, when a developer slightly modifies or alters a program published on GitHub or the like, a new verification logical formula v is generated without changing the overlapping parts (common parts) of the verification logical formula v before and after the modification or alteration. This has the effect of reducing the data size of the verification logical formula and improving the work efficiency of the developer and verifier.

〔supplement〕
The present invention is not limited to the above-described embodiment, and may have the following configurations or processes (operations).

(1) Each of the above programs can be recorded on a (non-temporary) recording medium or provided via a network such as the Internet.

(2) The CPU 101 in FIG. 2 may be a single CPU or multiple CPUs.

10 Proof verification system 30, 30a, 30b, 30c Proof terminal 31 Acquisition unit 32 Compiler 34b, 34c Labeling information generation unit 35a, 35b, 35c Logical formula generation unit 36 Proof creation unit 39 Output unit 51 Acquisition unit 56 Proof confirmation unit 59 Execution unit

Claims (4)

A proof verification system having a proof terminal for proving the safety of a program written in a high-level language and a verification terminal for verifying the safety of the program,
The certification terminal is
A compiler that generates an executable file based on the source code of the program;
a logical expression generating unit that generates an intermediate representation based on a source code of the program, and generates a verification logical expression indicating a condition that should be satisfied immediately before and immediately after an executable file of the program is executed, based on the intermediate representation and confidential definition information indicating that a predetermined variable name in the high-level language is confidential information;
a proof creation unit that proves that the executable file satisfies the condition based on the verification logical formula and creates a safety proof to guarantee the safety of the executable file;
an output unit that outputs the executable file, the verification formula, and the security proof;
having
The verification terminal includes:
a proof confirmation unit that confirms that the safety proof obtained from the certification terminal exists if the executable file satisfies the condition based on the verification logical formula;
having
Proof verification system. A proof verification system having a proof terminal for proving the safety of a program written in a high-level language and a verification terminal for verifying the safety of the program,
The certification terminal is
a compiler for generating an executable file based on the source code of the program in the high-level language;
a labeling information generation unit that generates auxiliary information, which is an intermediate representation, based on confidential definition information indicating that a predetermined variable name in the high-level language is confidential information, and generates labeling information, based on the auxiliary information, including a variable name in the auxiliary information and a label indicating that the variable name in the intermediate representation is the confidential information;
a logical expression generating unit that generates an intermediate representation based on a source code of the program in the high-level language, and generates a verification logical expression indicating a condition that should be satisfied immediately before and immediately after an executable file of the program is executed, based on the intermediate representation in the high-level language and the labeling information;
a proof creation unit that proves that the executable file satisfies the condition based on the verification logical formula and creates a safety proof to guarantee the safety of the executable file;
an output unit that outputs the executable file, the verification formula, and the security proof;
having
The verification terminal includes:
a proof confirmation unit that confirms that the safety proof obtained from the certification terminal exists if the executable file satisfies the condition based on the verification logical formula;
having
Proof verification system. A proof verification system having a proof terminal for proving the safety of a program written in a high-level language and a verification terminal for verifying the safety of the program,
a compiler for generating an executable file based on the modified source code of the high-level language program;
a labeling information generating unit that generates labeling information including a variable name in the second auxiliary information and a label indicating that the variable name in the intermediate representation is the confidential information, based on first auxiliary information, which is an intermediate representation generated by another certification terminal based on first confidential definition information indicating that a predetermined variable name in the high-level language before the change is confidential information, and second auxiliary information, which is an intermediate representation generated based on second confidential definition information indicating that a predetermined variable name in the high-level language after the change is confidential information;
a logical expression generating unit that generates a verification logical expression indicating a condition that should be satisfied immediately before and immediately after an executable file of the program is executed, based on a first intermediate representation generated by the other proving terminal based on a source code of the high-level language program before the change, a second intermediate representation generated based on the source code of the high-level language program after the change, and the labeling information;
a proof creation unit that proves that the executable file satisfies the condition based on the verification logical formula and creates a safety proof to guarantee the safety of the executable file;
an output unit that outputs the executable file, the verification formula, and the security proof;
having
The verification terminal includes:
a proof confirmation unit that confirms that the safety proof obtained from the certification terminal exists when the execution file satisfies the condition based on the verification logical formula.
Proof verification system. A proof verification method executed by a proof verification system having a proof terminal for proving the safety of a program written in a high-level language and a verification terminal for verifying the safety of the program, comprising:
The certification terminal is
A compilation process for generating an executable file based on the source code of the program;
a logical expression generation process for generating an intermediate representation based on a source code of the program, and generating a verification logical expression indicating a condition that should be satisfied immediately before and immediately after an executable file of the program is executed, based on the intermediate representation and confidential definition information indicating confidentiality that indicates that a predetermined variable name in the high-level language is confidential information;
a proof creation process for proving that the executable file satisfies the condition based on the verification logical formula and creating a safety proof for guaranteeing the safety of the executable file;
an output process for outputting the executable file, the verification formula, and the security proof;
Run
The verification terminal includes:
a proof verification process for verifying that the safety proof obtained from the certification terminal exists if the executable file satisfies the condition based on the verification logical formula;
Execute
Proof verification method.

Images