Transcript ppt

MOPS: an Infrastructure
for Examining Security
Properties of Software
Authors
Hao Chen and David Wagner
Appears in
ACM Conference on Computer and
Communications Security, 2002
Presented by
Peter Matthews
Software Vulnerabilities

Several causes


Certain bugs like buffer overflows may be avoided
by use of a type-safe language or use of boundschecking libraries
Another class of security bugs involve misuse of
higher level semantics



Many OS system calls have implicit constraints on
how they should be called
If this is not done, vulnerabilities may be introduced
This the class MOPS addresses
An example
// Current directory is “/var/ftp/”
chroot(“/var/ftp/pub”);
chdir(“/var/ftp/pub”);
filename= read_from_network();
/
fd = open(filename, O_RDONLY);
After chdir() call, current working directory is
still /var/ftp
If filename = “…/…/etc/passwd”, will not
restrict access!
Must call chdir(“/”) after chroot() to ensure
security
/var
/etc
/var/ftp
/etc/paswd
/var/ftp/pub
Temporal Safety Properties





Dictates the order of a sequence of security-relevant
operations
Can encode many rules of secure programming
Violating such properties may render a program
vulnerable to attack
Manual checking difficult in large programs
Detecting violations of these properties or verifying
the satisfaction of them would significantly help
reduce the frequency of software vulnerabilities
MOPS



A program analysis tool that allows one to
make temporal safety properties explicit and
verify whether they are properly respected by
source code
Determines any execution path through a
program that may violate a security property
Uses techniques from model checking and
program analysis to do so
(Very) Short Formal Model
Review

Finite State Automaton (FSA)
Input String
1
S1
1
0
1
0
1
0
S2
0

Pushdown Automaton (PDA)

Adds a stack, and allows transitions to interact with
this stack
Stack
Formal Model




 : The set of security-relevant operations
*
B   : All sequences of security operations that
violate the security property
*
T   : The set of all feasible execution paths of
the program
Assume that B is a regular language

There exists a FSA, M, that accepts B


B  L(M )
Assume that T is a context-free language

There exists a PDA, P, that accepts T

T  L(P )
Formal Model Continued…




Question is now: L( M )  L( P )  
This is also a context free language
Efficient algorithms to compute intersection of PDA
and FSA, and also to determine if the language
accepted by a PDA is empty
{T  B)}  {( M )  L( P)}



May give false alarms, but will not overlook a violation of
the security property
General problem is undecidable
Authors claim that false alarms are minimized
Example FSA
chdir(“/”)
Other
S3
S2
S1
chroot
Other
Another example of a
Temporal Security Property



Since a privileged process has full access
permission to the system, it should not make
system calls that run untrusted programs
without first dropping all privileges
One such system call: execl()
Should first call seteuid(!0)
Modular Implementation

Model process privilege
Other

Seteuid(0)
S2
S1
Other
Seteuid(!0)
Model execl()
Other
Other
S2
S1
Execl()
Execl()
Modular Composition

Mops automatically combines the two
Modeling Execution

MOPS models control flow

e.g. IF-THEN-ELSE


MOPS does not model data flow




MOPS pursues all paths
Does not provide offending input
Could possibly pursue impossible paths
Pointer points to position of next statement
Stack records return addresses of function
calls
Example Violating Program
1.
2.
5.
3.
4.
Execution Path Output
Modeling Operating System
Semantics


Difficult to construct accurately because of
increasing complexity, differences among
operating systems, and incomplete/incorrect
documentation
Instead construct directly from kernel code

First, determine the relevant kernel variables,
create states in FSA based on these variables


Done by hand
Then, determine the transitions among these
states

Done by MOPS, state-space explorer automatically
creates all transitions
Testing Real Applications

Performance



Sendmail 8.12.0 has 53k lines of code
MOPS spent 110 seconds parsing the source
code, and 95 seconds in model checking
Checking proper dropping privilege



sendmail 8.10.1 fails to drop privilege in user IDs
sendmail 8.12.0 fails to drop privilege in group
IDs
Known vulnerabilities
Strengths of Approach






Proposes concept of temporal security properties &
novel application of automata theory
Provably sound approach guarantees violations will
be found, given some constraints
Scalable, efficient algorithm
Can be used as a verification and bug-finding tool
Expansible, customizable approach
Comes with numerous example FSA’s


Missing string termination in context of strncat & strncpy
Insecure tempfile creation
Weaknesses of Approach




Can only test portable, single-threaded
applications without dynamic code generation
Data flow insensitivity means does not handle
function pointers, signal handlers, and nonlocal jumps
Possibility of false positives due to modeling
imprecision
Construction of further FSA’s is “non-trivial”
Possible Improvements


Pursue incorporation of data flow analysis
into model checking
Creation of repository of temporal safety
property models, allow access to and
contribution by members of the public
Questions?