| dc.description.abstract | Statically verifying behavioral properties of programs is an important research problem. An
efficient solution to this problem will have visible effects over multiple domains, ranging from
program development, program debugging, program correction and verification, etc. Type
systems are the most prevalently used static, light-weight verification systems for verifying
certain properties of programs. Unfortunately, simple types are inadequate at verifying many
behavioral/dynamic properties of programs. Typestates can tame this inadequacy of simple
types by associating each type in a programming language with a state information. However,
there are two major challenges in statically analyzing and verifying typestate properties over
programs.
The first challenge may be attributed to \increasing complexity of programs". The original
work on typestates can only verify/analyze a typestate property over very simple programs
which lacked dynamic memory allocation or aliasing. Subsequently, the following works on
typestates extended and improvised the analysis over programs with aliasing and heaps. However,
the state-of-the-art static typestate analysis works still cannot handle formidably rich
programming features like asynchrony, library calls and callbacks, concurrency, etc. The second
challenge may be attributed to \complexity of the property being verified". The original
and the current notion of typestates can only verify a property de nable through a finite-state
abstraction. This makes the state-of-the-art typestate analysis and verification works inadequate
to verify useful but richer non-regular program properties. For example, using classical
typestates we can verify a property like, \pop be called on a stack only after a push operation",
but we cannot verify a non-regular program property like, \number of push operations should
be at least equal to the number of pop operations". Currently, these behavioral properties are
mostly verified/enforced by programmers at runtime via explicit checks. Unfortunately, these
runtime checks are costly, error-prone, and lay an extra burden on the programmer.
In this thesis we take small steps towards tackling both these challenges. Addressing complex
program features, we present an asynchrony-aware static analysis, taking Android applications
as our use case. Android applications have convoluted control
flow, and complex features like asynchronous inter-component communications, library callbacks, Android enforced control flows (called as lifecycles), resource XMLs, which de ne and register event-handlers etc. Unfortunately,
none of the available static analysis works for Android soundly captures all these
features. We provide a formal semantics for Android asynchronous control
flow, capturing
these features. We use this semantics to introduce an intermediate program representation for
Android applications, called the Android Inter-Component Control Flow Graph (AICCFG),
and develop an asynchrony-aware interprocedural static analysis framework for Android applications.
We use this framework to develop a static typestate analysis to capture Android
resource API usage protocol violations. We present a set of benchmark applications for different
resource types, and empirically compare our typestate analysis with the state-of-the-art
synchronous static analyses for Android applications.
Addressing the challenges associated with increasing complexity of properties, we present an
expressive notion of typestates called, Parameterized typestates (p-typestates). p-typestates,
associate an extra Pressburger de nable property along with states of regular typestates. This
allows p-typestates to express many useful non-regular properties. We formally de ne this
notion of p-typestates, and a p-typestate property automaton, to represent a p-typestate property.
We present a dependent type system for these parameterized typestates and present
a simple typestate-oriented language incorporating p-typestates. Further, typechecking such
rich p-typestate properties require a programmer to provide invariants for loops and recursive
structures. Unfortunately, providing these invariants is a non-trivial task even for expert programmers.
To solve this problem, we present a simple and novel loop invariant calculation
approach for Pressburger de nable systems. We encode a number of real-world programs in
our dependently-typed language and use p-typestates type system, and loop-invariant calculation
to verify several rich properties which are not amenable to regular typestate analysis and
verification.
Finally we discuss several possible extensions of our thesis along both these directions | en_US |
