Difference between revisions of "Static analysis"
| Line 1: | Line 1: | ||
'''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dynamic analysis''', which basically means testing the software by running it on sample cases in the hope of exercising a bug. | '''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dynamic analysis''', which basically means testing the software by running it on sample cases in the hope of exercising a bug. | ||
| + | ==Caveats== | ||
Certain commercial providers call “static analysis” any check based on the source code of the program, including stylistic checks (e.g. presence of comments at any function entry, statistics on loop nests, and so on). In contrast, the analysis that we do inside the STATOR project is sound and based on the semantics of the program — meaning that if the analysis tool concludes, for instance, that some type conversion cannot overflow because the range of the value does not exceed that of the target type, this this is true for all execution of the program. “Sound” means that our analysis will never ignore some cases that are actually possible in the program, so if it says that some problem does not occur, then it ''cannot'' occur (in some sense, it has proved that it cannot occur). Many commercial tools will instead provide ''false negatives'' — failing to point some issue that the tool is claimed to detect. | Certain commercial providers call “static analysis” any check based on the source code of the program, including stylistic checks (e.g. presence of comments at any function entry, statistics on loop nests, and so on). In contrast, the analysis that we do inside the STATOR project is sound and based on the semantics of the program — meaning that if the analysis tool concludes, for instance, that some type conversion cannot overflow because the range of the value does not exceed that of the target type, this this is true for all execution of the program. “Sound” means that our analysis will never ignore some cases that are actually possible in the program, so if it says that some problem does not occur, then it ''cannot'' occur (in some sense, it has proved that it cannot occur). Many commercial tools will instead provide ''false negatives'' — failing to point some issue that the tool is claimed to detect. | ||
| − | This sounds too good to be true, and you may think there should be a catch. There are actually several. The main one is that a tool cannot be both sound and ''complete'' — here, completeness means that the tool is capable of proving any true property of the program. This means that a sound tool will fail to prove some properties, thus issuing warnings about problems that do not exist in the real system — ''false positives'' or ''false alarms''. This is unavoidable, as it is a consequence of mathematical properties of [[wikipedia:computable function|computable functions]] (the mathematical constructs underlying computer programs), more precisely of [[wikipedia:Rice's theorem|Rice's theorem]]. | + | This sounds too good to be true, and you may think there should be a catch. There are actually several. |
| + | |||
| + | The main one is that a tool cannot be both sound and ''complete'' — here, completeness means that the tool is capable of proving any true property of the program. This means that a sound tool will fail to prove some properties, thus issuing warnings about problems that do not exist in the real system — ''false positives'' or ''false alarms''. This is unavoidable, as it is a consequence of mathematical properties of [[wikipedia:computable function|computable functions]] (the mathematical constructs underlying computer programs), more precisely of [[wikipedia:Rice's theorem|Rice's theorem]]. | ||
| + | |||
| + | Another issue is that research tools, and also some commercial tools, often make simplifying assumptions about computer programs so as to make matters easier. For instance, the tool may assume that all integer computations operate over mathematical integers (ℤ), or that all floating-point computations operate over mathematical reals (ℝ). It may also assume some cleanliness about memory usage and pointer arithmetic. Tools such as [[Astrée]] or [http://www.mathworks.fr/products/polyspace/ PolySpace] try to be faithful to machine models in this respect. | ||
| + | |||
| + | Finally, an analyzer is a complex piece of software, which means that it most probably contains bugs. This is why the [http://verasco.imag.fr VERASCO project], a sister project of CompCert, is building a tool that is proved correct using the [[wikipedia:Coq|Coq]] proof assistant. Due to the sheer difficulty of such a task, however, VERASCO is looking to build into this tool only established static analysis techniques, while STATOR aims at developing cutting-edge approaches and algorithms. | ||
Revision as of 21:27, 25 October 2012
Static analysis is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to dynamic analysis, which basically means testing the software by running it on sample cases in the hope of exercising a bug.
Caveats
Certain commercial providers call “static analysis” any check based on the source code of the program, including stylistic checks (e.g. presence of comments at any function entry, statistics on loop nests, and so on). In contrast, the analysis that we do inside the STATOR project is sound and based on the semantics of the program — meaning that if the analysis tool concludes, for instance, that some type conversion cannot overflow because the range of the value does not exceed that of the target type, this this is true for all execution of the program. “Sound” means that our analysis will never ignore some cases that are actually possible in the program, so if it says that some problem does not occur, then it cannot occur (in some sense, it has proved that it cannot occur). Many commercial tools will instead provide false negatives — failing to point some issue that the tool is claimed to detect.
This sounds too good to be true, and you may think there should be a catch. There are actually several.
The main one is that a tool cannot be both sound and complete — here, completeness means that the tool is capable of proving any true property of the program. This means that a sound tool will fail to prove some properties, thus issuing warnings about problems that do not exist in the real system — false positives or false alarms. This is unavoidable, as it is a consequence of mathematical properties of computable functions (the mathematical constructs underlying computer programs), more precisely of Rice's theorem.
Another issue is that research tools, and also some commercial tools, often make simplifying assumptions about computer programs so as to make matters easier. For instance, the tool may assume that all integer computations operate over mathematical integers (ℤ), or that all floating-point computations operate over mathematical reals (ℝ). It may also assume some cleanliness about memory usage and pointer arithmetic. Tools such as Astrée or PolySpace try to be faithful to machine models in this respect.
Finally, an analyzer is a complex piece of software, which means that it most probably contains bugs. This is why the VERASCO project, a sister project of CompCert, is building a tool that is proved correct using the Coq proof assistant. Due to the sheer difficulty of such a task, however, VERASCO is looking to build into this tool only established static analysis techniques, while STATOR aims at developing cutting-edge approaches and algorithms.
