Publications

Peer-reviewed publications

  • M. Dimjašević, F. Howar, K. Luckow, and Z. Rakamarić, “Study of integrating random and symbolic testing for object-oriented software,” in Proceedings of the International Conference on integrated Formal Methods (iFM), 2018.
    [BibTeX] [Abstract]

    Testing is currently the main technique adopted by the industry for improving the quality, reliability, and security of software. In order to lower the cost of manual testing, automatic testing techniques have been devised, such as random and symbolic testing, with their respective trade-offs. For example, random testing excels at fast global exploration of software, while it plateaus when faced with hard-to-hit numerically-intensive execution paths. On the other hand, symbolic testing excels at exploring such paths, while it struggles when faced with complex heap class structures. In this paper, we describe an approach for automatic unit testing of object-oriented software that integrates the two techniques. We leverage feedback-directed unit testing to generate meaningful sequences of constructor+method invocations that create rich heap structures, and we in turn further explore these sequences using dynamic symbolic execution. We implement this approach in a tool called JDoop, which we augment with several parameters for fine-tuning its heuristics; such “knobs” allow for a detailed exploration of the various trade-offs that the proposed integration offers. Using JDoop, we perform an extensive empirical exploration of this space, and we describe lessons learned and guidelines for future research efforts in this area.

    @inproceedings{ifm2018-dhkz,
    author = {Marko Dimja\v{s}evi\'c and Falk Howar and Kasper Luckow and Zvonimir Rakamari\'c},
    title = {Study of Integrating Random and Symbolic Testing for Object-Oriented Software},
    booktitle = {Proceedings of the {International} {Conference} on integrated {Formal} {Methods} {(iFM)}},
    abstract = {Testing is currently the main technique adopted by the industry for improving the quality, reliability, and security of software. In order to lower the cost of manual testing, automatic testing techniques have been devised, such as random and symbolic testing, with their respective trade-offs. For example, random testing excels at fast global exploration of software, while it plateaus when faced with hard-to-hit numerically-intensive execution paths. On the other hand, symbolic testing excels at exploring such paths, while it struggles when faced with complex heap class structures. In this paper, we describe an approach for automatic unit testing of object-oriented software that integrates the two techniques. We leverage feedback-directed unit testing to generate meaningful sequences of constructor+method invocations that create rich heap structures, and we in turn further explore these sequences using dynamic symbolic execution. We implement this approach in a tool called JDoop, which we augment with several parameters for fine-tuning its heuristics; such "knobs" allow for a detailed exploration of the various trade-offs that the proposed integration offers. Using JDoop, we perform an extensive empirical exploration of this space, and we describe lessons learned and guidelines for future research efforts in this area.},
    year = {2018}
    }

  • K. Luckow, M. Dimjašević, D. Giannakopoulou, F. Howar, M. Isberner, T. Kahsai, Z. Rakamarić, and V. Raman, “JDart: a dynamic symbolic analysis framework,” in Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016. doi:10.1007/978-3-662-49674-9_26
    [BibTeX] [Abstract] [Download PDF]

    We describe JDart, a dynamic symbolic analysis framework for Java. A distinguishing feature of JDart is its modular architecture: the main component that performs dynamic exploration communicates with a component that efficiently constructs constraints and that interfaces with constraint solvers. These components can easily be extended or modified to support multiple constraint solvers or different exploration strategies. Moreover, JDart has been engineered for robustness, driven by the need to handle complex NASA software. These characteristics, together with its recent open sourcing, make JDart an ideal platform for research and experimentation. In the current release, JDart supports the Coral, SMTInterpol, and Z3 solvers, and is able to handle NASA software with constraints containing bit operations, floating point arithmetic, and complex arithmetic operations (e.g., trigonometric and nonlinear). We illustrate how JDart has been used to support other analysis techniques, such as automated interface generation and testing of libraries. Finally, we demonstrate the versatility and effectiveness of JDart, and compare it with state-of-the-art dynamic or pure symbolic execution engines through an extensive experimental evaluation.

    @inproceedings{tacas2016-ldghikrr,
    author = {Kasper Luckow and Marko Dimja\v{s}evi\'c and Dimitra Giannakopoulou and Falk Howar and Malte Isberner and Temesghen Kahsai and Zvonimir Rakamari\'c and Vishwanath Raman},
    title = {{JDart}: A Dynamic Symbolic Analysis Framework},
    doi = {10.1007/978-3-662-49674-9_26},
    booktitle = {Proceedings of the {International} {Conference} on {Tools} and {Algorithms} for the {Construction} and {Analysis} of {Systems} ({TACAS})},
    abstract = {We describe JDart, a dynamic symbolic analysis framework for Java. A distinguishing feature of JDart is its modular architecture: the main component that performs dynamic exploration communicates with a component that efficiently constructs constraints and that interfaces with constraint solvers. These components can easily be extended or modified to support multiple constraint solvers or different exploration strategies. Moreover, JDart has been engineered for robustness, driven by the need to handle complex NASA software. These characteristics, together with its recent open sourcing, make JDart an ideal platform for research and experimentation. In the current release, JDart supports the Coral, SMTInterpol, and Z3 solvers, and is able to handle NASA software with constraints containing bit operations, floating point arithmetic, and complex arithmetic operations (e.g., trigonometric and nonlinear). We illustrate how JDart has been used to support other analysis techniques, such as automated interface generation and testing of libraries. Finally, we demonstrate the versatility and effectiveness of JDart, and compare it with state-of-the-art dynamic or pure symbolic execution engines through an extensive experimental evaluation.},
    year = {2016},
    url = {https://dimjasevic.net/marko/wp-content/papercite-data/pdf/tacas2016-ldghikrr.pdf},
    }

  • M. Dimjašević, S. Atzeni, I. Ugrina, and Z. Rakamarić, “Evaluation of android malware detection based on system calls,” in Proceedings of the International Workshop on Security and Privacy Analytics (IWSPA), 2016. doi:10.1145/2875475.2875487
    [BibTeX] [Abstract] [Download PDF]

    With Android being the most widespread mobile platform, protecting it against malicious applications is essential. Android users typically install applications from large remote repositories, which provides ample opportunities for malicious newcomers. In this paper, we propose a simple, and yet highly effective technique for detecting malicious Android applications on a repository level. Our technique performs automatic classification based on tracking system calls while applications are executed in a sandbox environment. We implemented the technique in a tool called maline, and performed extensive empirical evaluation on a suite of around 12,000 applications. The evaluation yields an overall detection accuracy of 93% with a 5% benign application classification error, while results are improved to a 96% detection accuracy with up-sampling. This indicates that our technique is viable to be used in practice. Finally, we show that even simplistic feature choices are highly effective, suggesting that more heavyweight approaches should be thoroughly (re)evaluated.

    @inproceedings{iwspa2016-daur,
    author = {Marko Dimja\v{s}evi\'c and Simone Atzeni and Ivo Ugrina and Zvonimir Rakamari\'c},
    title = {Evaluation of Android Malware Detection Based on System Calls},
    doi = {10.1145/2875475.2875487},
    booktitle = {Proceedings of the {International} {Workshop} on {Security} and {Privacy} {Analytics} ({IWSPA})},
    abstract = {With Android being the most widespread mobile platform, protecting it against malicious applications is essential. Android users typically install applications from large remote repositories, which provides ample opportunities for malicious newcomers. In this paper, we propose a simple, and yet highly effective technique for detecting malicious Android applications on a repository level. Our technique performs automatic classification based on tracking system calls while applications are executed in a sandbox environment. We implemented the technique in a tool called maline, and performed extensive empirical evaluation on a suite of around 12,000 applications. The evaluation yields an overall detection accuracy of 93% with a 5% benign application classification error, while results are improved to a 96% detection accuracy with up-sampling. This indicates that our technique is viable to be used in practice. Finally, we show that even simplistic feature choices are highly effective, suggesting that more heavyweight approaches should be thoroughly (re)evaluated.},
    year = {2016},
    url = {https://dimjasevic.net/marko/wp-content/papercite-data/pdf/iwspa2016-daur.pdf},
    }

  • M. Dimjašević and D. 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. doi:10.1145/2771783.2771804
    [BibTeX] [Abstract] [Download PDF]

    This paper addresses the problem of specifying properties of aircraft separation assurance software, and verifying these properties at runtime. In particular, we target AutoResolver, a large, complex air-traffic control system that predicts and resolves aircraft loss of separation. In previous work, we developed a light-weight testing environment for AutoResolver. Our work contributed a wrapper around AutoResolver, which enabled the automated generation and fast execution of hundreds of thousands of tests. The focus of the work presented here is in specifying requirements for AutoResolver, in ensuring the generation of test cases that cover these requirements, and in developing a runtime infrastructure for automatically checking the requirements. Such infrastructure must be completely transparent to the AutoResolver code base. Our work combines test-case generation and runtime verification in innovative ways in order to address these challenges. The paper includes a detailed evaluation and discussion of our verification effort.

    @inproceedings{issta2015-dg,
    author = {Marko Dimja\v{s}evi\'c and Dimitra Giannakopoulou},
    title = {Test-Case Generation for Runtime Analysis and Vice Versa: Verification of Aircraft Separation Assurance},
    doi = {10.1145/2771783.2771804},
    booktitle = {Proceedings of the {International} {Symposium} on {Software} {Testing} and {Analysis} ({ISSTA})},
    abstract = {This paper addresses the problem of specifying properties of aircraft separation assurance software, and verifying these properties at runtime. In particular, we target AutoResolver, a large, complex air-traffic control system that predicts and resolves aircraft loss of separation. In previous work, we developed a light-weight testing environment for AutoResolver. Our work contributed a wrapper around AutoResolver, which enabled the automated generation and fast execution of hundreds of thousands of tests. The focus of the work presented here is in specifying requirements for AutoResolver, in ensuring the generation of test cases that cover these requirements, and in developing a runtime infrastructure for automatically checking the requirements. Such infrastructure must be completely transparent to the AutoResolver code base. Our work combines test-case generation and runtime verification in innovative ways in order to address these challenges. The paper includes a detailed evaluation and discussion of our verification effort.},
    year = {2015},
    url = {https://dimjasevic.net/marko/wp-content/papercite-data/pdf/issta2015-dg.pdf}
    }

  • M. Dimjašević, D. Giannakopoulou, F. Howar, M. Isberner, Z. Rakamarić, and V. Raman, “The Dart, the Psyco, and the Doop: concolic execution in Java Pathfinder and its applications,” in Proceedings of the java pathfinder workshop (jpf), 2014. doi:10.1145/2693208.2693248
    [BibTeX] [Abstract] [Download PDF]

    JDart is a concolic execution extension for Java PathFinder. Concolic execution executes programs with concrete values while recording symbolic constraints. In this way, it combines the benefits of fast concrete execution, with the possibility of generating new concrete values, triggered by symbolic constraints, in order to exercise additional, potentially rare, program behaviors. As is typical with concolic execution engines, JDart can be used for test-case generation. Beyond this basic mode, it has also been used as a component of other tools. In this paper, we describe the main features of JDart, provide usage examples, and give an overview of applications that use JDart. We particularly concentrate on our efforts into making JDart robust enough to handle large, complex systems.

    @inproceedings{jpf2014-dghirr,
    author = {Marko Dimja\v{s}evi\'c and Dimitra Giannakopoulou and Falk Howar and Malte Isberner
    and Zvonimir Rakamari\'c and Vishwanath Raman},
    title = {The {Dart}, the {Psyco}, and the {Doop}: Concolic Execution in {Java} {Pathfinder} and its Applications},
    doi = {10.1145/2693208.2693248},
    booktitle = {Proceedings of the Java Pathfinder Workshop (JPF)},
    abstract = {JDart is a concolic execution extension for Java PathFinder. Concolic execution executes programs with concrete values while recording symbolic constraints. In this way, it combines the benefits of fast concrete execution, with the possibility of generating new concrete values, triggered by symbolic constraints, in order to exercise additional, potentially rare, program behaviors. As is typical with concolic execution engines, JDart can be used for test-case generation. Beyond this basic mode, it has also been used as a component of other tools. In this paper, we describe the main features of JDart, provide usage examples, and give an overview of applications that use JDart. We particularly concentrate on our efforts into making JDart robust enough to handle large, complex systems.},
    year = {2014},
    url = {https://dimjasevic.net/marko/wp-content/papercite-data/pdf/jpf2014-dghirr.pdf}
    }

  • M. Dimjašević and Z. Rakamarić, “JPF-Doop: combining concolic and random testing for java,” in Java pathfinder workshop (jpf), 2013.
    [BibTeX] [Abstract] [Download PDF]

    Achieving high code coverage during software testing is important because it gives a measure of how thoroughly the software has been tested. However, reaching high code coverage in testing of real-world software is challenging due to its size and complexity. Our paper addresses this challenge by proposing an automatic multipronged approach. In particular, we propose an iterative algorithm for generating unit tests that meaningfully combines concolic execution and random testing. The algorithm aims to exploit the advantages of both random testing and systematic software verification techniques. We implemented the algorithm by integrating a Java Pathfinder’s concolic execution engine and Randoop, and dubbed the implementation JPF-Doop. Preliminary experimental results show that JPF-Doop outperforms Randoop in terms of code coverage.

    @inproceedings{jpf2013-dr,
    author = {Marko Dimja\v{s}evi\'c and Zvonimir Rakamari\'c},
    title = {{JPF-Doop}: Combining Concolic and Random Testing for Java},
    booktitle = {Java Pathfinder Workshop (JPF)},
    abstract = {Achieving high code coverage during software testing is important because it gives a measure of how thoroughly the software has been tested. However, reaching high code coverage in testing of real-world software is challenging due to its size and complexity. Our paper addresses this challenge by proposing an automatic multipronged approach. In particular, we propose an iterative algorithm for generating unit tests that meaningfully combines concolic execution and random testing. The algorithm aims to exploit the advantages of both random testing and systematic software verification techniques. We implemented the algorithm by integrating a Java Pathfinder’s concolic execution engine and Randoop, and dubbed the implementation JPF-Doop. Preliminary experimental results show that JPF-Doop outperforms Randoop in terms of code coverage.},
    year = {2013},
    note = {Extended abstract},
    url = {https://dimjasevic.net/marko/wp-content/papercite-data/pdf/jpf2013-dr.pdf}
    }

  • M. Dimjašević, “Automatic testing of software libraries,” in Formal methods in computer-aided design (FMCAD), 2013.
    [BibTeX] [Abstract] [Download PDF]

    Achieving high code coverage during software testing is important because code coverage gives a measure of how thoroughly the software has been tested. However, reaching high code coverage in testing of real-world software is challenging due to its size and complexity. This research addresses the challenge of reaching high code coverage by proposing two automatic approaches. One is an iterative algorithm for generating unit tests with concolic execution and random testing. The algorithm exploits both random testing and systematic software verification techniques. Preliminary results show the algorithm outperforms existing techniques. The other approach, which is our future work, uses automata learning to learn a component interface and to generate unit tests based on the learned interface.

    @inproceedings{fmcad2013-d,
    author = {Marko Dimja\v{s}evi\'c},
    title = {Automatic Testing of Software Libraries},
    booktitle = {Formal Methods in Computer-Aided Design ({FMCAD})},
    abstract = {Achieving high code coverage during software testing is important because code coverage gives a measure of how thoroughly the software has been tested. However, reaching high code coverage in testing of real-world software is challenging due to its size and complexity. This research addresses the challenge of reaching high code coverage by proposing two automatic approaches. One is an iterative algorithm for generating unit tests with concolic execution and random testing. The algorithm exploits both random testing and systematic software verification techniques. Preliminary results show the algorithm outperforms existing techniques. The other approach, which is our future work, uses automata learning to learn a component interface and to generate unit tests based on the learned interface.},
    year = {2013},
    note = {Extended abstract},
    url = {https://dimjasevic.net/marko/wp-content/papercite-data/pdf/fmcad2013-d.pdf}
    }

Technical Reports

  • M. Dimjašević, S. Atzeni, I. Ugrina, and Z. Rakamarić, “Android malware detection based on system calls,” University of Utah, School of Computing, UUCS-15-003, 2015.
    [BibTeX] [Abstract] [Download PDF]

    With Android being the most widespread mobile platform, protecting it against malicious applications is essential. Android users typically install applications from large remote repositories, which provides ample opportunities for malicious newcomers. In this paper, we propose a simple, and yet highly effective technique for detecting malicious Android applications on a repository level. Our technique performs automatic classification based on tracking system calls while applications are executed in a sandbox environment. We implemented the technique in a tool called maline, and performed extensive empirical evaluation on a suite of around 12,000 applications. The evaluation yields an overall detection accuracy of 93\% with a 5\% benign application classification error, while results are improved to a 96\% detection accuracy with up-sampling. This indicates that our technique is viable to be used in practice. Finally, we show that even simplistic feature choices are highly effective, suggesting that more heavyweight approaches should be thoroughly (re)evaluated.

    @techreport{maline-tr,
    author = {Dimja\v{s}evi\'{c}, Marko and Atzeni, Simone and Ugrina, Ivo and Rakamari\'{c}, Zvonimir},
    title = {Android Malware Detection Based on System Calls},
    abstract = {With Android being the most widespread mobile platform, protecting it against malicious applications is essential. Android users typically install applications from large remote repositories, which provides ample opportunities for malicious newcomers. In this paper, we propose a simple, and yet highly effective technique for detecting malicious Android applications on a repository level. Our technique performs automatic classification based on tracking system calls while applications are executed in a sandbox environment. We implemented the technique in a tool called maline, and performed extensive empirical evaluation on a suite of around 12,000 applications. The evaluation yields an overall detection accuracy of 93\% with a 5\% benign application classification error, while results are improved to a 96\% detection accuracy with up-sampling. This indicates that our technique is viable to be used in practice. Finally, we show that even simplistic feature choices are highly effective, suggesting that more heavyweight approaches should be thoroughly (re)evaluated.},
    institution = {University of Utah, School of Computing},
    number = {UUCS-15-003},
    year = {2015},
    url = {https://dimjasevic.net/marko/wp-content/papercite-data/pdf/maline-tr.pdf}
    }