Education
Ph.D. Computer Sceience (Summa cum laude), RISC and DK, Johannes Kepler University, Linz, Austria
M.Sc. Advanced Distributed Systems (Distinction), University of Leicester, UK
M.Sc. Computer Science (First Division), Islamia University Bahawalpur, Pakistan
Current Research
The goal of my current research is to develop a system which allows target systems to continue rendering useful
services even after successful (known or unknown) attack happens. The project is lead by Howard Shrobe (AIRE research group) and is an extension to AWDRAT middleware which is funded by DARPA's SRS (Self-Regenerative System) program. The motivation here is that today' cybersecurity tools are very limited as they are retrospective (i.e. catch things we have already seen) and focus on individual exploits instead of complex and multi-stage full campaign of an APT.
Past Research
In this project, we have developed a novel framework for the formal specification and
verification of MiniMaple programs and its application to a non-trivial program
package. MiniMaple is a substantial subset of the language of the computer
algebra system Maple; in contrast to Maple (which is dynamically typed), we have
equipped MiniMaple with a static type system. The main goal of the thesis is the
application of light-weight formal methods to MiniMaple programs (annotated with
types and behavioral specifications) for finding internal inconsistencies and
violations of methods preconditions by employing static program analysis. This
task is more complex for a computer algebra language like Maple as it supports
non-standard types of objects and also requires abstract data types to model
algebraic concepts and notions.
As a starting point, we have defined and formalized the syntax, semantics, type
system and specification language for MiniMaple. For verification, we
automatically translate the annotated MiniMaple program into (a semantically
equivalent program in) the intermediate language Why3ML of the verification tool
Why3; from the translated program, Why3 generates verification conditions whose
correctness can be proved by various automatic and interactive theorem provers
(e.g. Z3 and Coq). Furthermore, we have defined a denotational semantics of
MiniMaple and proved the soundness of the translation with respect to the
operational semantics of Why3ML. Finally, we discuss the application of our
verification framework to the Maple package DifferenceDifferential developed at
our institute to compute bivariate difference-differential dimension polynomials
using relative Groebner bases.
This research was carried out in the frame of project "Space Link Extension Service Management", which was sponsored and run by various space agencies, e.g.
NASA, USA. The goal of the project was to study the (space mission communication protocols) specification documents provided by NASA and to
- find ambiguities and inconsistencies in the requirements of the protocols
- devise a unified protocol resolving the identified ambiguities
- specify the behavior of the proposed protocol and finally
- to verify various properties of the protocol, e.g. absence of dead-lock and information inconsistencies.
Teaching
Currenlty, I am also working as an Associate Tutor (for distance learning modules) with the Univrsity of Leicester, UK.
Publications
The list of recent publications in reverse chronological order.