Research Summary
Marko Dimjašević
October 27, 2015
So far I have worked on several projects, which I briefly outline below.
For my
thesis I have been working on analyzing the Bluetooth stack in Android.
The main challenge is to verify properties across multiple software layers,
which range from applications and their libraries written in Java, down to the
operating system and drivers written in C. Therefore, we are looking at ways to learn an interface of each layer and
compose this information into a cross-language verification. We rely on our experience and tools in automatic software testing.
Thoroughly testing software such that
it covers as much of code as possible remains a major challenge. Towards addressing the challenge, we combined dynamic symbolic execution and
random testing for automatic software testing in order to be able to reach
both deep and hard to reach program states [1,2]. Recently we modularized JDart [3], the dynamic symbolic
execution tool we rely on in our approach; a tool paper is under submission.
Widespread use of mobile platforms makes them
an appealing target for attackers.We developed a technique for automatic analysis and detection of malicious
applications [4]. The technique combines automatic software testing, operating system-level
interfaces, machine learning, and an insight which models information flow in
an application execution. This work is under submission.
The US federal government's project aims to
create a new national airspace system that will be able to handle a two to
three-fold increase in air traffic. As part of the project, NASA has been developing a software system for
air-traffic control. We developed a runtime verification technique [5] for test
case generation and verification of such a complex system. This technique greatly improves an old debugging process in NASA that was
manual, error-prone, and that did not scale.
- 1
-
Marko Dimjašević.
Automatic testing of software libraries.
In Formal Methods in Computer-Aided Design (FMCAD), 2013.
Extended abstract.
- 2
-
Marko Dimjašević and Zvonimir Rakamarić.
JPF-Doop: Combining concolic and random testing for java.
In Java Pathfinder Workshop (JPF), 2013.
Extended abstract.
- 3
-
Marko Dimjašević, Dimitra Giannakopoulou, Falk Howar, Malte Isberner,
Zvonimir Rakamarić, and Vishwanath Raman.
The Dart, the Psyco, and the Doop.
In Proceedings of the Java Pathfinder Workshop (JPF), 2014.
- 4
-
Marko Dimjašević, Simone Atzeni, Ivo Ugrina, and Zvonimir
Rakamarić.
Android malware detection based on system calls.
Technical Report UUCS-15-003, University of Utah, School of
Computing, 2015.
- 5
-
Marko Dimjašević and Dimitra Giannakopoulou.
Test-case generation for runtime analysis and vice versa:
Verification of aircraft separation assurance.
In Proceedings of the International Symposium on Software
Testing and Analysis (ISSTA), 2015.