Lecture 01

Systems and Software
Verification Laboratory
Software Security
Lucas Cordeiro
Department of Computer Science
lucas.cordeiro@manchester.ac.uk
Career Summary
1 4
BSc/MSc in
Engineering and
Lecturer
Career Summary
1 2
BSc/MSc in MSc in Embedded

Engineering and Systems
Lecturer
Career Summary
1 2 3 4
BSc/MSc in MSc in Embedded Configuration and Feature Leader

Engineering and Systems Build Manager
Lecturer
Career Summary
1 2 3 4

Lecturer
Set-top Box
Software Engineer
Career Summary
1,7 2 3 4

Lecturer
5 6
Set-top Box PhD in Computer

Software Engineer Science
Career Summary
1,7 2 3 4

Lecturer
5 6 8
Set-top Box PhD in Computer Postdoctoral

Software Engineer Science Researcher
Career Summary
1,7 2 3 4

Lecturer
5 6 8 9
Set-top Box PhD in Computer Postdoctoral Senior Lecturer

Software Engineer Science Researcher
Audience
This course unit introduces students to basic and
advanced approaches to formally build verified
trustworthy software systems
Audience
• Reliability: deliver services as specified

Audience

• Availability: deliver services when requested
Audience

• Safety: operate without harmful states
Audience

• Resilience: transform, renew, and recover in timely
response to events
Audience

• Resilience: transform, renew, and recover in timely
response to events
• Security: remain protected against accidental or
deliberate attacks
Relationship to Other Courses
Software Security involves people and practices, to
build software systems, ensuring confidentiality,
integrity and availability
• Cyber-Security
• Cyber-Security
• Cryptography
• Cyber-Security
• Cryptography
• Automated Reasoning and Verification
• Cyber-Security
• Cryptography
• Logic and Modelling
• Cyber-Security
• Cryptography
• Agile and Test-Driven Development
• Cyber-Security
• Cryptography
• Software Engineering Concepts In Practice
• Cyber-Security
• Cryptography
• Software Engineering Concepts In Practice
• Systems Governance
Cyber-Security Pathway
Cyber-Security
Software Security Cryptography
Build programs that

continue to function System
correctly under Governance
malicious attack Trustworthy
SW Systems
Intended Learning Outcomes
• Explain computer security problem and why broken
software lies at its heart
• Explain continuous risk management and how to put it
into practice to ensure software security
• Introduce security properties into the software
development lifecycle
• Use software V&V techniques to detect software
vulnerabilities and mitigate against them
• Relate security V&V to risk analysis to address
continued resilience when a cyber-attack takes place
• Relate security V&V to risk analysis to address
continued resilience when a cyber-attack takes place
• Develop case studies to think like an attacker and
mitigate them using software V&V
Syllabus
• Part I: Software Security Fundamentals
o Defining a Discipline
o A Risk Management Framework
o Vulnerability Assessment and Management
o Overview on Traffic, Vulnerability and Malware Analysis
Syllabus (cont.)
• Part II: Software Security
o Architectural Risk Analysis
o Code Inspection for Finding Security Vulnerabilities and
Exposures (ref: Mitre’s CVE)
o Penetration Testing, Concolic Testing, Fuzzing, Automated
Test Generation
o Model Checking, Abstract Interpretation, Symbolic
Execution
o Risk-Based Security Testing and Verification
o Software Security Meets Security Operations
Syllabus (cont.)
• Part III: Software Security Grows Up
o Withstanding adversarial tactics and techniques defined in
Mitre’s ATT&CK™ knowledge base
o An Enterprise Software Security Program
Teaching Activities / Assessment
• Lectures will be available through slides, videos and
reading materials
• Lectures • Tutorials
• Workshops • Labs/Practicals
Teaching Activities / Assessment
• Lectures will be available through slides, videos and
reading materials
• Lectures • Tutorials
• Workshops • Labs/Practicals
• The full course will be assessed as follows:
• 70% Coursework
o Lab exercises = 40%
o Quizes = 10%
o Seminars = 20%
• 30% Exam
o Format: 2 hours, 3 questions, all the material.
Textbook
• McGraw, Gary: Software Security: Building Security
In, Addison-Wesley, 2006
Textbook
• Hoglund, Greg: Exploiting Software: How to Break
Code, Addison-Wesley, 2004
Textbook
• Hoglund, Greg: Exploiting Software: How to Break
Code, Addison-Wesley, 2004
• Ransome, James and Misra, Anmol: Core Software
Security: Security at the Source, CRC Press, 2014
Textbook
• Edmund M. Clark Jr., Orna Grumberg, Daniel Kroening,
Doron Peled, Helmut Veith: Model Checking, The MIT
Press, 2018
Textbook
Press, 2018
• Mark Dowd , John McDonald, et al.: The Art of
Software Security Assessment: Identifying and
Preventing Software Vulnerabilities, Addison-Wesley,
2006
Textbook
Press, 2018
• Mark Dowd , John McDonald, et al.: The Art of
Software Security Assessment: Identifying and
Preventing Software Vulnerabilities, Addison-Wesley,
2006
These slides are also based

on the lectures notes of
“Computer and
Network Security” by Dan
Boneh and John Mitchell.
Software Platform Security
https://www.cybok.org/media/downloads/cybok_version_1.0.pdf
SEI CERT C Coding Standard: Rules for
Developing Safe, Reliable, and Secure
Systems
https://resources.sei.cmu.edu/downloads/secure-coding/
assets/sei-cert-c-coding-standard-2016-v01.pdf
The CERT Division
• CERT’s main goal is to improve the security and
resilience of computer systems and networks
https://www.sei.cmu.edu/about/divisions/cert/
End of Admin
Most importantly,
ENJOY!
Intended Learning
Outcomes
• Define standard notions of security and use
them to evaluate the system’s confidentiality,
Intended Learning
Outcomes
• Explain standard software security problems
in real-world applications
Intended Learning
Outcomes
• Use testing and verification techniques to
reason about the system’s safety and security
Intended Learning
Outcomes
Motivating Example
void main(){
int x=getPassword();
int getPassword() { if(x){
char buf[4]; printf(“Access Denied\n”);
gets(buf); exit(0);
return strcmp(buf, ”SMT”); }
} printf(“Access Granted\n”);
}
• What happens if the user enters “SMT”?
Barrett et al., Problem Solving for the 21st Century, 2014.

Motivating Example
void main(){
gets(buf); exit(0);
}
• What happens if the user enters “SMT”?
• On a Linux x64 platform running GCC 4.8.2, an input consisting of 24

arbitrary characters followed by ], <ctrl-f>, and @, will bypass the
“Access Denied” message
• A more extended input will run over into other parts of the computer
memory
Barrett et al., Problem Solving for the 21st Century, 2014.

What is Safety and Security?
• Safety
– If the user supplies any input, then the system
generates the desired output
• Any input ⇒ Good output
• Safe and protected from danger/harm
• More features leads to a higher
verification effort
What is Safety and Security?
• Safety
– If the user supplies any input, then the system
generates the desired output
• Any input ⇒ Good output
• Safe and protected from danger/harm
verification effort
• Security
– If an attacker supplies unexpected input, then the
system does not fail in specific ways
• Bad input ⇒ Bad output
• Protection of individuals, organizations,
and properties against external threats
chance of attacks
Overview
System
User Attacker
• Security consists of the following basic elements:

– Honest user (Alice)
– Dishonest attacker
Boneh, D. and Mitchell, J., “Computer and Network Security”, 2009.

Overview
System
User Attacker
• Security consists of the following basic elements:

– Honest user (Alice)
– Dishonest attacker
– Goal: how the attacker
• disrupts Alice’s use of the system (Integrity, Availability)
• learns information intended for Alice only (Confidentiality)
Network Security
Network Attacker
System Intercepts and

controls network
communication
User
Web Security
System
Web Attacker
Sets up a malicious
site visited by the
victim; there exists
no control of the
User network

Operating System Security
OS Attacker
Controls malicious
files and
applications
User
CIA Principle
System
User Attacker
Confidentiality: Attacker does not learn the

user’s secrets.

CIA Principle
System
User Attacker

user’s secrets.
Integrity: Attacker does not undetectably
corrupt system’s function for the user

CIA Principle
System
User Attacker

user’s secrets.
Integrity: Attacker does not undetectably
corrupt system’s function for the user
Availability: Attacker does not keep system
from being useful to the user
What does it mean for software to
be secure?
• A software system is secure if it satisfies a specified
security objective
§ E.g. confidentiality, integrity and availability
requirements for the system’s data and functionality
What does it mean for software to
be secure?
• A software system is secure if it satisfies a specified
security objective
§ E.g. confidentiality, integrity and availability
requirements for the system’s data and functionality
Example of Social Networking Service

Confidentiality: Pictures posted by a user can only be seen
by that user’s friends
Integrity: A user can like any given post at most once
Availability: The service is operational more than 99.9% of
the time on average
Security Failure and Vulnerabilities
• A security failure is a scenario where the software

system does not achieve its security objective
– A vulnerability is the underlying cause of such a failure

• Most software systems do not have precise, explicit
security objectives
– These objectives are not absolute
– Traded off other objectives e.g. performance or usability

• Most software systems do not have precise, explicit
security objectives
– These objectives are not absolute
– Traded off other objectives e.g. performance or usability
• Software implementation bugs can lead to a
substantial disruption in the behaviour of the
software
Intended Learning
Outcomes

Software Security
• Software security consists of building programs that
continue to function correctly under malicious attack
Software
Requirements Definition
Application Availability services are
accessible if
requested by
Firmware authorized users
Integrity data completeness
OS and accuracy are
preserved
Services Confidentiality only authorized
users can get access
Communication to the data
Why are there security
vulnerabilities?
• Software is one of the sources of security problems
– Why do programmers write insecure code?
vulnerabilities?
• Awareness is the main issue
vulnerabilities?
• Some contributing factors

– Limited number of courses in computer security
vulnerabilities?

– Programming textbooks do not emphasize security
vulnerabilities?

– Limited number of security audits
vulnerabilities?

– Programmers are focused on implementing features
vulnerabilities?

– Security is expensive and takes time
vulnerabilities?

– Security is expensive and takes time
– Legacy software (e.g., C is an unsafe language)
Implementation Vulnerability
• We use the term implementation vulnerability (or

security bug) both for bugs that
– make it possible for an attacker to violate a security
objective
– for classes of bugs that enable specific attack techniques
Implementation Vulnerability
• We use the term implementation vulnerability (or

security bug) both for bugs that
– make it possible for an attacker to violate a security
objective
– for classes of bugs that enable specific attack techniques
• The Common Vulnerabilities and Exposures
(CVE) is a publicly available list of entries
– describes vulnerabilities in widely-used software
components
– it lists close to a hundred thousand such vulnerabilities
https://cve.mitre.org/
Critical Software Vulnerabilities
• Null pointer dereference
int main() {!
double *p = NULL;
int n = 8;!
for(int i = 0; i < n; ++i )
*(p+i) = i*2;!
return 0;!
}
int main() {! A NULL pointer dereference

double *p = NULL; occurs when the application
int n = 8;!
dereferences a pointer that it
for(int i = 0; i < n; ++i )
*(p+i) = i*2;! expects to be valid, but is
return 0;! NULL
}
int main() {! A NULL pointer dereference

double *p = NULL; occurs when the application
int n = 8;!
dereferences a pointer that it
for(int i = 0; i < n; ++i )
*(p+i) = i*2;! expects to be valid, but is
return 0;! NULL
}
Scope Impact
Availability Crash, exit and restart
Integrity Execute Unauthorized Code
Confidentiality or Commands
Availability

• Double free
int main(){!
char* ptr = (char *)malloc(sizeof(char));!
if(ptr==NULL) return -1;!
*ptr = 'a’;!
free(ptr);
free(ptr);!
return 0;!
}

• Double free
int main(){! The product calls free()
char* ptr = (char *)malloc(sizeof(char));! twice on the same
if(ptr==NULL) return -1;! memory address,
*ptr = 'a’;!
free(ptr);
leading to modification
free(ptr);! of unexpected memory
return 0;! locations
}

• Double free
int main(){! The product calls free()
char* ptr = (char *)malloc(sizeof(char));! twice on the same
if(ptr==NULL) return -1;! memory address,
*ptr = 'a’;!
free(ptr);
leading to modification
free(ptr);! of unexpected memory
return 0;! locations
}
Scope Impact
Integrity Execute Unauthorized Code
Confidentiality or Commands
Availability

• Double free
• Unchecked Return Value to NULL Pointer
Dereference
String username = getUserName();!
if (username.equals(ADMIN_USER)) {!
...!
}

• Double free
Dereference
The product does
String username = getUserName();! not check for an
...! error after calling a
} function that can
return with a NULL
pointer if the function
fails

• Double free
Dereference
The product does
String username = getUserName();! not check for an
...! error after calling a
} function that can
return with a NULL
pointer if the function
Scope Impact fails
Availability Crash, exit and restart

• Double free
Dereference
• Division by zero
• Missing free
• Use after free
• APIs rule based checking
Race Condition Vulnerabilities
VDU
VDU
VDU VDU
Race conditions
P P P P
occur when
multiple
processes
perform Process
unsynchronized
accesses to the Database
database
• Concurrency is an essential subject with importance

well beyond the area of cyber-security
– Prove program correctness

• Race condition vulnerabilities are relevant for many

different types of software
– Race conditions on the file system: privileged programs
• An attacker can invalidate the condition between the check and action

• Race condition vulnerabilities are relevant for many

different types of software
– Race conditions on the file system: privileged programs
• An attacker can invalidate the condition between the check and action
– Races on the session state in web applications: web

servers are often multi-threaded
• Two HTTP requests belonging to the same HTTP session may access the
session state concurrently (the corruption of the session state)
Web Application Vulnerabilities
https://www.imperva.com/blog/the-state-of-web-application-
vulnerabilities-in-2018/
Vulnerabilities by Categories
Structured output generation
vulnerabilities
• A SQL injection vulnerability is a structured output
generation vulnerability where the structured output
consists of SQL code
– These vulnerabilities are relevant for server-side web app
• interact with a back-end database by constructing queries
based on input provided through web forms
Structured output generation
vulnerabilities
• A SQL injection vulnerability is a structured output
generation vulnerability where the structured output
consists of SQL code
– These vulnerabilities are relevant for server-side web app
• interact with a back-end database by constructing queries
based on input provided through web forms
• A script injection vulnerability, or Cross-Site

Scripting (XSS) vulnerability is a structured output
generation vulnerability
– the structured output is JavaScript code sent to a web
browser for client-side execution
SQL Injection
• SQL injection allows an attacker to interfere with the

queries to the database in order to retrieve data
- retrieving hidden data

- subverting application logic
- UNION attacks
- examining the database
- blind SQL injection
https://portswigger.net/web-security/sql-injection
Example of SQL Injection
• A programmer can construct a SQL query to check

name and password as
query = "select * from users where

name=’" + name + "’" and pw = ’" +
password + "’"
Example of SQL Injection
• A programmer can construct a SQL query to check

name and password as
query = "select * from users where

name=’" + name + "’" and pw = ’" +
password + "’"
• However, if an attacker provides the name string, the

attacker can set name to “John’ –”
– this would remove the password check from the query
(note that -- starts a comment in SQL)
Cross-site Scripting (XSS)
• XSS attacks represent injection of malicious scripts

into trusted websites
<% String eid = request.getParameter("eid"); %>

...
Employee ID: <%= eid %>


...
• XSS allows attackers to bypass access controls

– If eid has a value that includes source code, then the
code will be executed by the web browser


...
• XSS allows attackers to bypass access controls

– If eid has a value that includes source code, then the
code will be executed by the web browser
– use e-mail or social engineering tricks to lead victims to
visit a link to another URL
XML External Entity (XXE) Processing
• XXE represents a malicious action against an

application that parses XML input
– XXE occurs when XML input (incl. an external entity) is
processed by a weakly configured XML parser
– XXE might lead to the disclosure of confidential data
<?xml version="1.0" encoding="ISO-8859-1"?>

<!DOCTYPE foo [ <!ELEMENT foo ANY > Disclosing /etc/passwd
<!ENTITY xxe SYSTEM "expect://id" >]>
<creds>
<user>&xxe;</user>
<pass>mypass</pass>
</creds> <?xml version="1.0" encoding="ISO-8859-1"?>
<!DOCTYPE foo [
<!ELEMENT foo ANY >
<!ENTITY xxe SYSTEM "file:///etc/passwd”
>]><foo>&xxe;</foo>
Denial of Service (DoS) Attack
• A DoS attack makes a machine or network resource

unavailable to its intended users

– Flood attacks occur when the system receives too much
traffic for the server to buffer, causing them to slow down
• Buffer overflow attacks: send more traffic to a network address
than the programmers have built the system to handle

– Flood attacks occur when the system receives too much
traffic for the server to buffer, causing them to slow down
• Buffer overflow attacks: send more traffic to a network address
than the programmers have built the system to handle
– Crashing attacks exploit vulnerabilities that cause the

target system or service to crash
• Input is sent that takes advantage of bugs in the target that
subsequently crash or severely destabilize the system so that it
cannot be accessed or used
Intended Learning
Outcomes

Proof by Induction
• Why is proof by induction relevant?

Proof by Induction

Proof by Induction

Proof by Induction
How do we prove this program is correct?

Proof by Induction of Programs
Why do we need to ensure software
security?
• Consumer electronic products
must be as robust and bug-free
Not only
as possible, given that even
safety-critical
medium product-return rates tend
systems
to be unacceptable
“Engineers reported the static

analyser Infer was key to build a
concurrent version of Facebook app
to the Android platform.”
- Peter O’Hearn, FLoC, 2018
Why do we need to ensure software
security?
• Consumer electronic products
must be as robust and bug-free
as possible, given that even
medium product-return rates tend
to be unacceptable
- In 2014, Apple revealed a bug known as Gotofail,
which was caused by a single misplaced “goto”
command in the code
- “Impact: An attacker with a privileged network

position may capture or modify data in sessions
protected by SSL/TLS”
– Apple Inc., 2014.
Industry NEEDS Formal Verification
“There has been a tremendous amount of

valuable research in formal methods, but
rarely have formal reasoning techniques
been deployed as part of the
development process of large industrial
codebases.”
- Peter O’Hearn, FLoC, 2018.
“Formal automated reasoning is one of

the investments that AWS is making in
order to facilitate continued simultaneous
growth in both functionality and security.”
- Byron Cook, FLoC, 2018.
Temporal Logic Model
Checking
• Model checking is an automatic verification
technique for finite state concurrent systems
Checking
• Developed independently by Clarke and Emerson
and by Queille and Sifakis in early 1980’s
Checking
• The assertions written as formulas in
propositional temporal logic (Pnueli 77)
Checking
• The assertions written as formulas in
propositional temporal logic (Pnueli 77)
• Verification procedure is algorithmic rather than
deductive in nature
Advantages of Model Checking
§ No proofs!!! (Algorithmic
rather than Deductive)
§ Fast (compared to other
rigorous methods such as
theorem proving)
theorem proving)
§ Diagnostic
counterexamples
theorem proving)
§ Diagnostic
counterexamples
§ No problem with partial
specifications
theorem proving)
§ Diagnostic
counterexamples
§ No problem with partial
specifications
§ Logics can easily express
many concurrency
properties
LTL - Linear Time Logic (Pn 77)
Determines Patterns on Infinite Traces
Atomic Propositions a
Boolean Operations
Temporal operators
a “a is true now”
Xa “a is true in the neXt state”
Fa “a will be true in the Future”
Ga “a will be Globally true in the future”
aUb “a will hold true Until b becomes true”
Boolean Operations
Temporal operators
Boolean Operations
Temporal operators
Atomic Propositions a a a a a
Boolean Operations
Temporal operators
Atomic Propositions a a a a b
Boolean Operations
Temporal operators
Model Checking Problem
• Let M be a state-transition graph.
• Let ƒ be an assertion or specification in

temporal logic.
• Find all states s of M such that M, s satisfies ƒ.
LTL Model Checking Complexity:

(Sistla, Clarke & Vardi, Wolper)
• singly exponential in size of specification
• linear in size of state-transition graph.
Trivial Example
Microwave Oven
State-transition graph
describes system evolving ~ Start
~ Close
over time. ~ Heat
~ Error
Start ~ Start
~ Start
~ Close Close
Close
~ Heat Heat
~ Heat
Error ~ Error
~ Error
Start Start Start

Close Close Close
~ Heat ~ Heat Heat
Error ~ Error ~ Error
Temporal Logic and Model
Checking
• The oven doesn’t heat up until the door is

closed.
• “Not heat_up holds until door_closed”
• (~ heat_up) U door_closed
Bounded Model Checking (BMC)
Basic idea: check negation of given property up to given depth
property
¬ϕ0 ∨ ¬ϕ1 ∨ ¬ϕ2 ∨ ¬ϕk-1 ∨ ¬ϕk
...
transition
system M0 M1 M2 Mk-1 Mk
counterexample trace bound
property
¬ϕ0 ∨ ¬ϕ1 ∨ ¬ϕ2 ∨ ¬ϕk-1 ∨ ¬ϕk
...
transition
• Transition system M unrolled k times

– for programs: loops, recursion, …
property
¬ϕ0 ∨ ¬ϕ1 ∨ ¬ϕ2 ∨ ¬ϕk-1 ∨ ¬ϕk
...
transition

• Translated into verification condition ψ such that
ψ satisfiable iff ϕ has counterexample of max. depth k
property
¬ϕ0 ∨ ¬ϕ1 ∨ ¬ϕ2 ∨ ¬ϕk-1 ∨ ¬ϕk
...
transition

• Translated into verification condition ψ such that
ψ satisfiable iff ϕ has counterexample of max. depth k
BMC has been applied successfully to
verify HW and SW
Satisfiability Modulo Theories
SMT decides the satisfiability of first-order logic formulae
using the combination of different background theories
Theory Example
Equality x1=x2 ∧ ¬ (x1=x3) ⇒ ¬(x1=x3)
Bit-vectors (b >> i) & 1 = 1
Linear arithmetic (4y1 + 3y2 ≥ 4) ∨ (y2 – 3y3 ≤ 3)
Arrays (j = k ∧ a[k]=2) ⇒ a[j]=2
Combined theories (j ≤ k ∧ a[j]=2) ⇒ a[i] < 3
int getPassword() {
Software BMC char buf[4];
gets(buf);
return strcmp(buf, ”ML”);
}
• program modelled as transition system void main(){
– state: pc and program variables int x=getPassword();
if(x){
– derived from control-flow graph printf(“Access Denied\n”);
exit(0);
– added safety properties as extra nodes }
printf(“Access Granted\n”);
• program unfolded up to given bounds }
• unfolded program optimized to reduce blow-up

– constant propagation
crucial
– forward substitutions
int getPassword() {
gets(buf);
}
if(x){
exit(0);

crucial
– forward substitutions
g1 = x1 == 0
• front-end converts unrolled and a1 = a0 WITH [i0:=0]
a2 = a0
optimized program into SSA a3 = a2 WITH [2+i0:=1]
a4 = g1 ? a1 : a3
t1 = a4 [1+i0] == 1
int getPassword() {
gets(buf);
}
if(x){
exit(0);

crucial
– forward substitutions ⎡ g1 := (x1 = 0) ⎤
⎢∧ a := store(a , i ,0) ⎥
• front-end converts unrolled and ⎢ 1 0 0 ⎥
C := ⎢∧ a2 := a0 ⎥
⎢ ⎥
optimized program into SSA ⎢∧ a3 := store(a2 ,2 + i0 ,1)⎥
⎢∧ a := ite( g , a , a ) ⎥
⎣ 4 1 1 3 ⎦
• extraction of constraints C and properties P ⎡i0 ≥ 0 ∧ i0 < 2 ⎤
⎢ ∧ 2 + i ≥ 0 ∧ 2 + i < 2⎥
– specific to selected SMT solver, uses theories P := ⎢
0 0
⎢∧ 1 + i0 ≥ 0 ∧ 1 + i0 < 2 ⎥
⎥
• satisfiability check of C ∧ ¬P
⎢ ⎥
⎣∧ select (a4 , i0 + 1) = 1 ⎦
Software BMC Applied to Security
void main(){ buffer overflow attack
gets(buf); exit(0);
}
Barrett et al., “Problem Solving for the 21st Century”, 2014.

gets(buf); exit(0);
}
SSA & loop unrolling
sp0,sp1,sp2:BITVECTOR(8);
ip:BITVECTOR(8);
m0,m1,m2,m3,m4,m5 : ARRAY BITVECTOR(8) OF BITVECTOR(8);
in : ARRAY INT OF BITVECTOR(8);
ASSERT sp1 = BVSUB(8,sp0,0bin100);
ASSERT m1 = m0 WITH [sp1] := in[1];
ASSERT m2 = m1 WITH [BVPLUS(8,sp1,0bin1)] := in[2];
ASSERT sp2 = BVPLUS(8,sp1,0bin100);
ASSERT ip = m5[sp2];
ASSERT NOT ip = m0[sp0];
CHECKSAT;
gets(buf); exit(0);
}
ip:BITVECTOR(8);
ASSERT sp1 = BVSUB(8,sp0,0bin100); 4-character array buf
ASSERT sp2 = BVPLUS(8,sp1,0bin100);
CHECKSAT;
gets(buf); exit(0);
}
ip:BITVECTOR(8);
ASSERT sp2 = BVPLUS(8,sp1,0bin100); reclaim the memory occupied by buf
CHECKSAT;
gets(buf); exit(0);
}
ip:BITVECTOR(8);
ASSERT ip = m5[sp2]; ip is loaded with the location pointed to by sp
CHECKSAT;
gets(buf); exit(0);
}
ip:BITVECTOR(8); We wish to determine
m0,m1,m2,m3,m4,m5 : ARRAY BITVECTOR(8) OF BITVECTOR(8); whether it is possible to
ASSERT sp1 = BVSUB(8,sp0,0bin100); 4-character array buf set ip to a value that we
ASSERT m1 = m0 WITH [sp1] := in[1]; choose instead of the
ASSERT m2 = m1 WITH [BVPLUS(8,sp1,0bin1)] := in[2]; location of the if
statement
ASSERT ip = m5[sp2]; ip is loaded with the location pointed to by sp
CHECKSAT;
Context-Bounded Model Checking
Idea: iteratively generate all possible interleavings and call

the BMC procedure on each interleaving
... combines
• symbolic model checking: on each individual interleaving
• explicit state model checking: explore all interleavings
– bound the number of context switches allowed among
threads
Context-Bounded Model Checking
Idea: iteratively generate all possible interleavings and call

the BMC procedure on each interleaving
... combines
• symbolic model checking: on each individual interleaving
• explicit state model checking: explore all interleavings
– bound the number of context switches allowed among
threads
… implements
• symbolic state hashing (SHA1 hashes)
• monotonic partial order reduction that combines dynamic POR
with symbolic state space exploration
Lazy Exploration of the Reachability Tree
υ0 : tmain,0, active thread, context bound
initial state val1=0, val2=0,
m1=0, m2=0,… global and local variables
υ1: ttwoStage,1, syntax-directed

val1=0, val2=0,
expansion rules
m1=1, m2=0,…
CS1
CS2
execution paths
υ1: ttwoStage,1, syntax-directed

val1=0, val2=0,
expansion rules
m1=1, m2=0,…
CS1
υ2: ttwoStage,2,
val1=1, val2=0,
m1=1, m2=0,… interleaving completed, so
call single-threaded
CS2 BMC
execution paths
υ1: ttwoStage,1,
val1=0, val2=0, backtrack to last unexpanded node
m1=1, m2=0,…
and continue
CS1
υ2: ttwoStage,2, υ3: treader,2,

val1=1, val2=0, val1=0, val2=0,
m1=1, m2=0,… m1=1, m2=0,…
CS2
execution paths
blocked execution paths (eliminated)
υ1: ttwoStage,1,
val1=0, val2=0, backtrack to last unexpanded node
m1=1, m2=0,…
and continue
CS1

val1=1, val2=0, val1=0, val2=0,
m1=1, m2=0,… m1=1, m2=0,… symbolic execution can statically
determine that path is blocked
CS2
(encoded in instrumented mutex-op)
execution paths

val1=0, val2=0, val1=0, val2=0,
m1=1, m2=0,… m1=1, m2=0,…
CS1
υ2: ttwoStage,2, υ3: treader,2, υ5: ttwoStage,2, υ6: treader,2,

val1=1, val2=0, val1=0, val2=0, val1=0, val2=0, val1=0, val2=0,
m1=1, m2=0,… m1=1, m2=0,… m1=1, m2=0,… m1=1, m2=0,…
CS2
execution paths
Predicate Abstraction
• It abstracts data by only keeping track of certain
predicates to represent the data
Initial Abstraction Verification
C/C++ Concurrent
Program Boolean Model Property
with threads Program Checker holds
CEGAR Refinement Spurious?

Bug
found
Framework
Initial Abstraction Verification
C/C++ Concurrent
Program Boolean Model Property
with threads Program Checker holds
CEGAR Refinement Spurious?

Bug
found
Framework
• Conservative approach reduces the state space,

but generates spurious counter-examples
Example for Predicate
Abstraction
void main() {
int main() { bool p1, p2;
int i;
p1=TRUE;
i=0; p2=TRUE;
}
while(even(i))
i++; + p1 ⇔ i=0
p2 ⇔ even(i) = while(p2)
{
p1=p1?FALSE:nondet();
p2=!p2;
}
}
C program Predicates Boolean program

[Graf, Saidi ’97]
[Ball, Rajamani ’01]
Combine Simulation and
Verification
• Improve coverage and reduce verification time by
combining static and dynamic verification
Verification
Embedded Software
Specification Microprocessor
model
Verification
Verification Techniques
Embedded Software Simulation
Specification Microprocessor Formal Verification

model
Verification
Verification Techniques
Embedded Software Simulation
Specification Microprocessor Formal Verification

model
Combine
Coverage Improve
Quiz about Software Security
Go to https://kahoot.it/
Summary
• Defined the term security and use them to

evaluate the system’s confidentiality, integrity
and availability
• Demonstrated the importance of verification and
validation techniques to ensure software security
properties
• Application of model checking and coverage test
generation for security

Lecture 01

Uploaded by

Copyright:

Available Formats

Lecture 01

Uploaded by

Document Information

Original Title

Copyright

Available Formats

Share this document

Share or Embed Document

Sharing Options

Did you find this document useful?

Is this content inappropriate?

Copyright:

Available Formats

Lecture 01

Uploaded by

Copyright:

Available Formats

Systems and Software

BSc/MSc in MSc in Embedded

BSc/MSc in MSc in Embedded Configuration and Feature Leader

BSc/MSc in MSc in Embedded Configuration and Feature Leader

BSc/MSc in MSc in Embedded Configuration and Feature Leader

Set-top Box PhD in Computer

BSc/MSc in MSc in Embedded Configuration and Feature Leader

Set-top Box PhD in Computer Postdoctoral

BSc/MSc in MSc in Embedded Configuration and Feature Leader

Set-top Box PhD in Computer Postdoctoral Senior Lecturer

• Reliability: deliver services as specified

• Reliability: deliver services as specified

• Reliability: deliver services as specified

• Reliability: deliver services as specified

• Reliability: deliver services as specified

Software Security Cryptography

Build programs that

• The full course will be assessed as follows:

These slides are also based

• What happens if the user enters “SMT”?

Barrett et al., Problem Solving for the 21st Century, 2014.

• What happens if the user enters “SMT”?

• On a Linux x64 platform running GCC 4.8.2, an input consisting of 24

Barrett et al., Problem Solving for the 21st Century, 2014.

• Security consists of the following basic elements:

Boneh, D. and Mitchell, J., “Computer and Network Security”, 2009.

• Security consists of the following basic elements:

System Intercepts and

Boneh, D. and Mitchell, J., “Computer and Network Security”, 2009.

Confidentiality: Attacker does not learn the

Boneh, D. and Mitchell, J., “Computer and Network Security”, 2009.

Confidentiality: Attacker does not learn the

Boneh, D. and Mitchell, J., “Computer and Network Security”, 2009.

Confidentiality: Attacker does not learn the

Example of Social Networking Service

• A security failure is a scenario where the software

• A security failure is a scenario where the software

• A security failure is a scenario where the software

• Define standard notions of security and use

• Some contributing factors

• Some contributing factors

• Some contributing factors

• Some contributing factors

• Some contributing factors

• Some contributing factors

• We use the term implementation vulnerability (or

• We use the term implementation vulnerability (or

• Null pointer dereference

• Null pointer dereference

int main() {! A NULL pointer dereference

• Null pointer dereference

int main() {! A NULL pointer dereference

• Null pointer dereference

• Null pointer dereference

• Null pointer dereference

• Null pointer dereference

• Null pointer dereference

• Null pointer dereference

• Null pointer dereference