| 书目名称 | Symbolic Execution and Quantitative Reasoning | | 副标题 | Applications to Soft | | 编辑 | Corina S. Pasareanu | | 视频video | | | 丛书名称 | Synthesis Lectures on Software Engineering | | 图书封面 |  | | 描述 | .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 probab | | 出版日期 | Book 2020 | | 版次 | 1 | | doi | https://doi.org/10.1007/978-3-031-02551-8 | | isbn_softcover | 978-3-031-01423-9 | | isbn_ebook | 978-3-031-02551-8Series ISSN 2328-3319 Series E-ISSN 2328-3327 | | issn_series | 2328-3319 | | copyright | Springer Nature Switzerland AG 2020 |
| 1 |
Front Matter |
|
|
Abstract
|
| 2 |
,Introduction, |
Corina S. Pasareanu |
|
Abstract
In today’s world, software systems have become more pervasive and complex leading to an increased need for techniques and tools that can ensure the safety and security of such systems. Testing is the most commonly used techniques for finding errors and vulnerabilities in software. However, it is typically a costly, manual process that accounts for a large fraction of software development and maintenance costs and often fails to uncover subtle, low-probability errors. Symbolic execution is a program analysis technique that can be used to automate software testing by systematically generating test inputs that can exercise (or “cover”) large portions of the program and can thus help finding many subtle program errors.
|
| 3 |
,Symbolic Execution: The Basics, |
Corina S. Pasareanu |
|
Abstract
In this chapter, I give a gentle introduction to symbolic execution, using the simple example illustrated in Figure 2.1. On the left-hand side of the figure, there is some code that takes two integer inputs x and y and it checks . is greater than y, in which case some computation is performed to swap the two inputs. After this computation, x is checked again to see if it is greater than y, in which case an assert violation will happen. If the code swapping works correctly, this assert violation should not be possible. Testing this program for assert violations would typically involve assigning some concrete values to the inputs (say x = 1 and y = 2) and executing the code. As a result, only . program path will be executed; that does not lead to the error.
|
| 4 |
,Symbolic Complexity Analysis, |
Corina S. Pasareanu |
|
Abstract
In this chapter I will talk about the application of symbolic execution to the analysis of non-functional properties of software systems with an emphasis on the analysis of worst-case algorithmic complexity in programs. The presentation follows [29]. The problem is to identify the program inputs that lead to the . execution time or memory consumed by a program. Understanding such worst-case executions is important, as it can reveal performance bottlenecks in the program and it can also point out opportunities for program optimizations. Also of serious concern are . that are due to algorithmic complexity, allowing a malicious user to easily build a “small” input that causes the system to consume an impractically large amount of resources (time or memory). By exploiting these vulnerabilities an adversary can mount Denial-of-Service (DoS) attacks in order to deny service to the system’s benign users or to disable the system. Algorithmic complexity vulnerabilities are often the consequence of the algorithms used rather than of traditional “software bugs,” and consequently traditional software bug hunting techniques are of little use to address them. Profilers can be used for finding pe
|
| 5 |
,Probabilistic Reasoning, |
Corina S. Pasareanu |
|
Abstract
Symbolic execution typically involves exploring program paths and checking . along each program path, leading to increased code coverage and to the discovery of assert violations and other run-time errors that may be present in the analyzed program. Symbolic execution can also be used to find worst-case behavior as discussed in the previous chapter. Let us study techniques that aim to not only find such paths but to also quantify . paths satisfy certain properties. More precisely, the goal of these techniques is to estimate . it is for a program to satisfy given properties.
|
| 6 |
,Side-Channel Analysis, |
Corina S. Pasareanu |
|
Abstract
In this chapter I touch upon the application of symbolic execution and probabilistic reasoning in the security domain, namely for the analysis of side channels in programs. Side channels enable a malicious user to recover secret program data from non-functional characteristics of computations, such as time or power consumption, number of memory accesses, or size of output files. Side-channel attacks have been shown to pose serious threats, e.g., by recovering cryptographic keys from the RSA encryption/decryption algorithm [9], and private information about users, as with commonly used algorithms for data compression [24]. There is thus an increased need for practical tools that can detect and prevent side-channel vulnerabilities.
|
| 7 |
,Conclusion and Directions for the Future, |
Corina S. Pasareanu |
|
Abstract
In this book I described symbolic execution and highlighted some of its applications to the analysis of programs, with the goal of ensuring their safety and security. These applications include software bug and vulnerability detection, complexity analysis, reliability analysis, and side-channel quantification and attack synthesis.
|
| 8 |
Back Matter |
|
|
Abstract
|
|
|
发表于 2025-3-21 19:14:32
