Muutke küpsiste eelistusi

E-raamat: String Analysis for Software Verification and Security

, , ,
  • Formaat: PDF+DRM
  • Ilmumisaeg: 04-Jan-2018
  • Kirjastus: Springer International Publishing AG
  • Keel: eng
  • ISBN-13: 9783319686707
Teised raamatud teemal:
  • Formaat - PDF+DRM
  • Hind: 67,91 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
String Analysis for Software Verification and SecuritySuurem pilt
  • Formaat: PDF+DRM
  • Ilmumisaeg: 04-Jan-2018
  • Kirjastus: Springer International Publishing AG
  • Keel: eng
  • ISBN-13: 9783319686707
Teised raamatud teemal:

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

This book discusses automated string-analysis techniques, focusing particularly on automata-based static string analysis. It covers the following topics: automata-bases string analysis, computing pre and post-conditions of basic string operations using automata, symbolic representation of automata, forward and backward string analysis using symbolic automata representation, constraint-based string analysis, string constraint solvers, relational string analysis, vulnerability detection using string analysis, string abstractions, differential string analysis, and automated sanitization synthesis using string analysis.

String manipulation is a crucial part of modern software systems; for example, it is used extensively in input validation and sanitization and in dynamic code and query generation. The goal of string-analysis techniques and this book is to determine the set of values that string expressions can take during program execution. String analysis can be used to solve many problems in modern software systems that relate to string manipulation, such as: (1) Identifying security vulnerabilities by checking if a security sensitive function can receive an input string that contains an exploit; (2) Identifying possible behaviors of a program by identifying possible values for dynamically generated code; (3) Identifying html generation errors by computing the html code generated by web applications; (4) Identifying the set of queries that are sent to back-end database by analyzing the code that generates the SQL queries; (5) Patching input validation and sanitization functions by automatically synthesizing repairs illustrated in this book.

Like many other program-analysis problems, it is not possible to solve the string analysis problem precisely (i.e., it is not possible to precisely determine the set of string values that can reach a program point). However, one can compute over- or under-approximations of possible string values. If the approximations are precise enough, they can enable developers to demonstrate existence or absence of bugs in string manipulating code. String analysis has been an active research area in the last decade, resulting in a wide variety of string-analysis techniques.

This book will primarily target researchers and professionals working in computer security, software verification, formal methods, software engineering and program analysis. Advanced level students or instructors teaching or studying courses in computer security, software verification or program analysis will find this book useful as a secondary text.

Arvustused

The book can be said to be tailored as a handy manual for researchers looking for algebraic approaches based on the manipulation of regular expressions (in a large sense) and on solving string constraints, over inputs provided by users in web applications, for handling security issues in these applications. (Siva Anantharaman, Mathematical Reviews, November, 2019)

1 Introduction
1(14)
1.1 Common Vulnerabilities Due to String Manipulation Errors
4(2)
1.2 Examples of String Manipulating Code and Errors
6(6)
1.3 Overview
12(3)
2 String Manipulating Programs and Difficulty of Their Analysis
15(8)
2.1 A Simple String Manipulation Language
15(1)
2.2 Automated and Precise Verification of String Programs Is Not Possible
16(2)
2.3 A Richer String Manipulation Language
18(4)
2.4 Summary
22(1)
3 State Space Exploration
23(14)
3.1 Semantics of String Manipulation Languages
23(3)
3.2 Explicit State Space Exploration
26(3)
3.2.1 Forward Reachability
27(1)
3.2.2 Backward Reachability
28(1)
3.3 Symbolic Exploration
29(6)
3.3.1 Symbolic Reachability
30(1)
3.3.2 Fixpoints
31(4)
3.4 Summary
35(2)
4 Automata Based String Analysis
37(20)
4.1 A Lattice for Sets of Strings
37(1)
4.2 Symbolic Reachability Analysis with Automata
38(3)
4.3 Symbolic Automata Representation
41(4)
4.3.1 MTBDD Representation
43(1)
4.3.2 Modeling Non-Determinism Using Symbolic DFA
44(1)
4.3.3 Symbolic vs. Explicit DFA
45(1)
4.4 Post-Condition Computation
45(6)
4.4.1 Concatenation and Replace Operations
46(1)
4.4.2 Post-Condition of Concatenation
47(1)
4.4.3 Post-Condition of Replacement
48(3)
4.5 Pre-Condition Computation
51(4)
4.5.1 Pre-Condition of Concatenation
51(2)
4.5.2 Pre-Condition of Replacement
53(2)
4.6 Summary
55(2)
5 Relational String Analysis
57(12)
5.1 Relations Among String Variables
57(2)
5.2 Multi-Track DFAs
59(1)
5.3 Relational String Analysis
59(2)
5.3.1 Word Equations
60(1)
5.4 Construction of Multi-Track DFAs for Basic Word Equations
61(4)
5.5 Symbolic Reachability Analysis
65(3)
5.5.1 Forward Fixpoint Computation
66(2)
5.5.2 Summarization
68(1)
5.6 Summary
68(1)
6 Abstraction and Approximation
69(14)
6.1 Regular Abstraction
69(1)
6.2 Alphabet Abstraction
70(4)
6.3 Relation Abstraction
74(2)
6.4 Composing Abstractions
76(1)
6.5 Automata Widening Operation
77(3)
6.6 Summary
80(3)
7 Constraint-Based String Analysis
83(20)
7.1 Symbolic Execution with String Constraints
83(4)
7.2 Automata-Based String Constraint Solving
87(6)
7.2.1 Mapping Constraints to Automata
87(6)
7.3 Relational Constraint Solving with Multi-Track DFA
93(3)
7.3.1 Relational String Constraint Solving
94(1)
7.3.2 Relational Integer Constraint Solving
95(1)
7.3.3 Mixed String and Integer Constraint Solving
95(1)
7.4 Model Counting
96(6)
7.4.1 Automata-Based Model Counting
99(2)
7.4.2 Counting All Solutions within a Given Bound
101(1)
7.5 Summary
102(1)
8 Vulnerability Detection and Sanitization Synthesis
103(20)
8.1 Vulnerability Detection and Repair
104(7)
8.2 Patching Algorithm
111(1)
8.3 Vulnerability Analysis
112(2)
8.4 Vulnerability Signatures
114(2)
8.5 Relational Signatures
116(3)
8.6 Sanitization Generation
119(3)
8.7 Summary
122(1)
9 Differential String Analysis and Repair
123(26)
9.1 Formal Modeling of Validation and Sanitization Functions
126(7)
9.1.1 Post- and Pre-Image of a Sanitizer
130(3)
9.2 Discovering Client- and Server-Side Input Validation and Sanitization Inconsistencies
133(3)
9.2.1 Extracting and Mapping Input Validation and Sanitization Functions at the Client- and the Server-Side
133(1)
9.2.2 Inconsistency Identification
134(2)
9.3 Semantic Differential Repair for Input Validation and Sanitization
136(11)
9.3.1 Differential Repair Problem
140(1)
9.3.2 Differential Repair Algorithm
141(6)
9.4 Summary
147(2)
10 Tools
149(6)
10.1 LibStranger
149(1)
10.2 Stranger
150(1)
10.3 SemRep
151(2)
10.4 ABC
153(2)
11 A Brief Survey of Related Work
155(10)
11.1 String Analysis
155(3)
11.1.1 Grammar Based String Analysis
155(2)
11.1.2 Automata-Based String Analysis
157(1)
11.1.3 Hybrid String Analysis
158(1)
11.2 String Constraint Solvers
158(3)
11.2.1 Automata-Based Solvers
159(1)
11.2.2 Bounded Solvers
160(1)
11.2.3 Combination of Theories
161(1)
11.2.4 Model Counting String Constraint Solvers
161(1)
11.3 Bug and Vulnerability Detection in Web Applications
161(2)
11.3.1 Client-Side Analysis
162(1)
11.3.2 Server-Side Analysis
162(1)
11.4 Differential Analysis and Repair
163(2)
11.4.1 Differential Analysis
163(1)
11.4.2 Differential Repair
164(1)
12 Conclusions
165(2)
References 167
Lisainfo e-raamatute kohta Lisainfo e-raamatute kohta
Püsilink: https://www.kriso.ee/db/97833196867072e.html
Märksõnad: