Detection device, detection method, and detection program
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.
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.