Software security problems are good candidates for application of verification techniques. Usually it is not a complex task to represent certain security-related property in a particular verification framework. For instance in any software model checking environment (MC)[1] it is possible to state buffer overflow detection as a reachability problem. The approach works in theory and in practice, but has a major scalability drawback: the state-space, which represents all possible behaviors of the system, might grow exponentially in the size of the product of a model and a property. From the other side MC has an important advantage - a counter-example is produced automatically when the bug is found. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Tsitovich, A. (2008). Detection of security vulnerabilities using guided model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5366 LNCS, pp. 822–823). https://doi.org/10.1007/978-3-540-89982-2_90
Mendeley helps you to discover research relevant for your work.