This book reviews recent advances in symbolic execution and its
probabilistic variant and discusses how they can be used to ensure the
safety and security of software systems. Symbolic execution is a
systematic program analysis technique which explores multiple program
behaviors all at once by collecting and solving symbolic constraints
collected from the branching conditions in the program. The obtained
solutions can be used as test inputs that execute feasible program
paths. Symbolic execution has found many applications in various
domains, such as security, smartphone applications, operating systems,
databases, and more recently deep neural networks, uncovering subtle
errors and unknown vulnerabilities. We review here the technique has
also been extended to reason about algorithmic complexity and resource
consumption. Furthermore, symbolic execution has been recently
extended with probabilistic reasoning, allowing one to reason about
quantitative properties of software systems. The approach computes the
conditions to reach target program events of interest and uses model
counting to quantify the fraction of the input domain satisfying these
conditions thus computing the probability of event occurrence. This
probabilistic information can be used for example to compute the
reliability of an aircraft controller under different wind conditions
(modeled probabilistically) or to quantify the leakage of sensitive
data in a software system, using information theory metrics such as
Shannon entropy. This book is intended for students and software
engineers who are interested in advanced techniques for testing and
verifying software systems.
Les mer
Applications to Software Safety and Security
Produktdetaljer
ISBN
9783031025518
Publisert
2022
Utgiver
Vendor
Springer
Språk
Product language
Engelsk
Format
Product format
Digital bok
Forfatter