US-12619739-B2 - Detection device, detection method, and detection program

US12619739B2US 12619739 B2US12619739 B2US 12619739B2US-12619739-B2

Abstract

An unsafe location enumeration unit ( 131 ) enumerates, based on a code of a program, locations that do not satisfy a predetermined condition indicating that type conversion is safe among locations where a type casting occurs in the program. A context extraction unit ( 132 ) transition an automaton corresponding to the locations enumerated by the unsafe location enumeration unit ( 131 ) and extract a context reaching the locations. A vulnerability verification unit ( 133 ) verifies whether the location extracted by the context extraction unit ( 132 ) satisfies an annotation prepared in advance.

Inventors

Tatsuhiro AOSHIMA
Toshinori USUI
Yuhei KAWAKOYA
Makoto Iwamura
Jun Miyoshi

Assignees

NTT, INC.

Dates

Publication Date: 20260505
Application Date: 20210427

Claims (20)

1 . A detection device comprising a processor configured to execute operations comprising: enumerating, based on a code of a program, a plurality of locations in the code of the program, wherein the plurality of locations does not satisfy a predetermined condition, and the predetermined condition indicates that type conversion is safe at the plurality of locations where a type casting occurs in the program; transitioning an automaton corresponding to the plurality of locations, wherein the automaton further includes a first sub automaton specifying a variable included in a conditional expression and a second sub automaton that indicates a structure of the conditional expression; extracting a context reaching the plurality of location and updates the automaton; verifying whether a location of the plurality of locations satisfies a predetermined annotation; and transmitting a result of verifying to an application configured to display the result of verifying the code of the program, wherein the result of verifying describes a type confusion vulnerability of the code of the program.
2 . The detection device according to claim 1 , wherein the enumerating further comprises determining a castable relation and a partial type relation in a casting source type and a casting destination type.
3 . The detection device according to claim 1 , wherein, when a variable appears during extraction of a conditional expression by the first sub automaton, the transitioning the automation further comprises specifying the variable using the second sub automaton, and the second sub automation specifies the variable.
4 . The detection device according to claim 1 , wherein the verifying further comprises verifying whether the location satisfies an annotation described by defining a condition of a union with a tag as a refinement type.
5 . The detection device according to according to claim 1 , wherein the code of the program represents a program code for execution by a computer, and the program code is expressed either in C language or C++ language.
6 . The detection device according to according to claim 1 , wherein the result of verifying indicates a location of type confusion vulnerability of the code of the program.
7 . The detection device according to according to claim 1 , wherein the predetermined annotation indicates a data structure describing a condition of a union with a tag as a refinement type of a code.
8 . A detection method, comprising: enumerating, based on a code of a program, a plurality of locations in the code of the program, wherein the plurality of locations does not satisfy a predetermined condition, and the predetermined condition indicates that type conversion is safe at the location where a type casting occurs in the program; transitioning an automaton corresponding to the plurality of locations, wherein the automaton further includes a first sub automaton specifying a variable included in a conditional expression and a second sub automaton that indicates a structure of the conditional expression; extracting a context reaching the plurality of locations and updates the automaton; verifying whether a location of the locations satisfies a predetermined annotation; and transmitting a result of verifying to an application configured to display the result of verifying the code of the program, wherein the result of verifying describes a type confusion vulnerability of the code of the program.
9 . The detection method of claim 8 , wherein the enumerating further comprises determining a castable relation and a partial type relation in a casting source type and a casting destination type.
10 . The detection method of claim 8 , wherein, when a variable appears during extraction of a conditional expression by the first sub automaton, the transitioning the automation further comprises specifying the variable using the second sub automaton, and the second sub automation specifies the variable.
11 . The detection method of claim 8 , wherein the verifying further comprises verifying whether the location satisfies an annotation described by defining a condition of a union with a tag as a refinement type.
12 . The detection method of claim 8 , wherein the code of the program represents a program code for execution by a computer, and the program code is expressed either in C language or C++ language.
13 . The detection method of claim 8 , wherein the predetermined annotation indicates a data structure describing a condition of a union with a tag as a refinement type of a code, and the result of verifying indicates a location of type confusion vulnerability of the code of the program.
14 . A computer-readable non-transitory recording medium storing computer-executable program instructions that when executed by a processor cause a computer to execute operations comprising: enumerating, based on a code of a program, a plurality of locations in the code of the program, wherein the plurality of locations does not satisfy a predetermined condition, and the predetermined condition indicates that type conversion is safe at the plurality of locations where a type casting occurs in the program; transitioning an automaton corresponding to the plurality of locations, wherein the automaton further includes a first sub automaton specifying a variable included in a conditional expression and a second sub automaton that indicates a structure of the conditional expression; extracting a context reaching the plurality of location and updates the automaton; and verifying whether a location of the plurality of locations satisfies a predetermined annotation; and transmitting a result of verifying to an application configured to display the result of verifying the code of the program, wherein the result of verifying describes a type confusion vulnerability of the code of the program.
15 . The computer-readable non-transitory recording medium according to claim 14 , wherein the enumerating further comprises determining a castable relation and a partial type relation in a casting source type and a casting destination type.
16 . The computer-readable non-transitory recording medium according to claim 14 , wherein, when a variable appears during extraction of a conditional expression by the first sub automaton, the transitioning the automation further comprises specifying the variable using the second sub automaton, and the second sub automation specifies the variable.
17 . The computer-readable non-transitory recording medium according to claim 14 , wherein the verifying further comprises verifying whether the location satisfies an annotation described by defining a condition of a union with a tag as a refinement type.
18 . The computer-readable non-transitory recording medium according to claim 14 , wherein the code of the program represents a program code for execution by a computer, and the program code is expressed either in C language or C++ language.
19 . The computer-readable non-transitory recording medium according to claim 14 , wherein the predetermined annotation indicates a data structure describing a condition of a union with a tag as a refinement type of a code.
20 . The computer-readable non-transitory recording medium according to claim 14 , wherein the result of verifying indicates a location of type confusion vulnerability of the code of the program.

Description

CROSS-REFERENCE TO RELATED APPLICATIONS This application is a U.S. 371 Application of International Patent Application No. PCT/JP2021/016864, filed on 27 Apr. 2021, the disclosure of which is hereby incorporated herein by reference in its entirety. TECHNICAL FIELD The present invention relates to a detection device, a detection method, and a detection program. BACKGROUND ART In the related art, a union type inspection technology for a subset of C language other than a pointer type is known (for example, see NPT 1). The technology described in NPT 1 extracts execution context from a conditional statement and a substitution statement while performing structural type inspection and verifies whether an extracted condition satisfies a union type specification using a theoretical solver. Further, the technology described in NPT 1 can cope with a pointer type by calculating candidates for an indicator of a pointer in combination with pointer analysis. The theoretical solver may be a satisfiability modulo theories (SMT) solver or the like. CITATION LIST Non Patent Literature [NPT 1] Jhala, R., et al. (2007), “State of the Union: Type Inference via Craig Interpolation.” TACAS. SUMMARY OF INVENTION Technical Problem However, in the technology of the related art, there is a problem that type confusion vulnerability may not be detected efficiently. The type confusion vulnerability is a bug in which a program confuses a data type. Since a computer expresses all data with 0 and 1, it cannot be distinguished whether the data is a numerical value, a character, or an image and the program determines a data type. Therefore, when a computer confuses an integer and a pointer, for example, a numerical value (integer) prepared by an attacker may be misunderstood as a numerical value (pointer) indicating a location address of data or the program. Accordingly, there is a risk that data leakage, alteration, and malicious arbitrary code execution will occur. For example, in the technology of the prior art, since it is assumed that there is no pointer, there is a problem that a union type value and a tag variable can be rewritten superficially via a completely different pointer variable. In addition, since an indicator of a pointer cannot be correctly calculated in pointer analysis, the candidates for the indicator of the pointer are missed or the candidates for the indicator of the pointer are infinite in some cases. Accordingly, vulnerability may be missed or analysis may not be finished. Further, types selected from union types are incompatible with each other (upcasting at C and C++ is not possible), and the conditions are also mutually exclusive (two or more conditions may not be all satisfied). Therefore, the technology of the related art cannot cope with classes having an inheritance relation such as C++ which is seen to be object-oriented. Solution to Problem In order to solve the foregoing problems and to achieve an objective, a detection device includes: an enumeration unit configured to enumerate, based on a code of a program, locations that do not satisfy a predetermined condition indicating that type conversion is safe among locations where a type casting occurs in the program; an extraction unit configured to transition an automaton corresponding to the locations enumerated by the enumeration unit and extract a context reaching the locations; and a verification unit configured to verify whether the location extracted by the extraction unit satisfies an annotation prepared in advance. Advantageous Effects of Invention According to the present invention, it is possible to effectively detect the type confusion vulnerability. BRIEF DESCRIPTION OF DRAWINGS FIG. 1 is a diagram illustrating an exemplary configuration of a detection device according to a first embodiment. FIG. 2 is a flowchart illustrating a flow of a detection process. FIG. 3 is a diagram illustrating an example of notation of a refinement type. FIG. 4 is a flowchart illustrating a flow of determination processing of a castable relation. FIG. 5 is a flowchart illustrating a flow of determination processing of a partial relation. FIG. 6 is a flowchart illustrating a flow of processing for a nested annotation. FIG. 7 is a diagram illustrating an example of a syntax of a descriptive language of an annotation. FIG. 8 is a diagram illustrating an example of an annotation. FIG. 9 is a diagram illustrating an exemplary operation. FIG. 10 is a diagram illustrating an example of a computer that executes a detection program. DESCRIPTION OF EMBODIMENTS Embodiments of a detection device, a detection method, and a detection program according to the present application will be described below in detail with reference to the drawings. The present invention is not limited to the embodiments to be described below. Configuration of First Embodiment First, a configuration of a detection device according to a first embodiment will be described with reference to FIG. 1. FIG. 1 is