Differences between revisions 8 and 9
Revision 8 as of 2016-03-25 04:50:32
Size: 7057
Editor: ?MarkoDimjasevic
Revision 9 as of 2016-03-25 06:13:36
Size: 7118
Editor: ?MarkoDimjasevic
Deletions are marked like this. Additions are marked like this.
Line 30: Line 30:
  1. A patch to Debile: https://github.com/opencollab/debile/pull/38   1. Two patches to Debile:
   * https://github.com/opencollab/debile/pull/44

Support for KLEE in Debile

  • Name: Marko Dimjašević

  • Contact/Email/IRC nick:

  • Background: I am a 4th year computer science PhD student at the University of Utah, USA (the UTC-6 timezone). I also did research at NASA. I do research in software verification in general and symbolic execution in particular (list of publications and conference talks). I'm fluent in C (15 years), Java (4 years), and Python (3 years), but I speak Bash (4 years) and C++ (15 years) too. For the last 10 years I've been a free software enthusiast and for the last 3 years a Debian user. Last year I started contributing to Debian by packaging software verification tools. I've contributed in code to several free software projects and in non-coding ways to a few as well, including KDE. I've coded in several programming languages, including C, Java, AspectJ, C++, Python, Bash, and R. I have some system administration skills as I host my email, web, and cloud services, and I've also worked on packaging software verification tools, as it can be seen on Alioth and mentors.d.n. A research project I've been working on is on applying the KLEE verification tool to real-world software. In 2012 and 2013 I successfully participated in Google Summer of Code as a student. With all that in mind, I believe I am a perfect candidate for this project, which I proposed to Debian. A list of my current and recent projects can be found on my website.

  • Project title: Support for KLEE in Debile

  • Project details: Debile is a Debian package analysis infrastructure. It can invoke a software analysis tool from a few supported tools that automatically analyzes a Debian package against a coding style or for common software errors such as a null pointer dereference. KLEE is a software analysis tool that performs symbolic execution of a target C program. The goal of this project is to add support for KLEE in Debile.

  • Synopsis: Writing and maintaining software is challenging. Software is complex and keeping it bug-free remains an unsolved problem. Debian Stretch, the next Debian stable release, comprises 850 million lines of software source code. Code written in the C programming language accounts for 41% of the lines, which is more than in any other programming language. Debile, Debian's package analysis platform, so far includes the ?CppCheck, Clang Static Analyzer, and Coccinelle tools for packages with C, C++, and Objective-C code. However, all of the tools perform static analyses, which can result in false positives. Too many reported false positives hinder adoption of the tools. To address this issue, I propose to integrate the KLEE tool into Debile. KLEE performs dynamic analysis on C programs and reports only true positives, i.e. real bugs. It does so by systematically exploring as many as possible execution paths in a given program. Errors that KLEE reports exist only along feasible execution paths, i.e. they correspond to real bugs in the program.

  • Benefits to Debian With Debian Stretch, the next stable release of Debian, having around 350 millions of lines of code written in C, a sound analysis tool KLEE for C programs integrated into Debian's package build infrastructure would be very appealing to Debian, as KLEE can automatically detect some categories of errors that evade a compiler's analysis. For every error KLEE detects it also generates a corresponding witness test case. Even if it will work for a fraction of all the C lines, it will still be very beneficial as it will make Debian more stable, robust, and secure.

  • Deliverables: The deliverables are a patch to the Debile system that adds support for KLEE.

  • Project schedule: I am expecting the project to last until the end of Google Summer of Code 2016. As I am hoping to become a Debian Developer eventually, I am planning to continue working on Debile even after GSoC is over. There are modifications that need to be done both to KLEE (such as implementing the Firehose file format) and to Debile (adding wrapping code to work with KLEE). I have already been working on the project - I have set up a Debile instance on my server, I have created initial versions of packages for KLEE and its so far not packaged dependency, I have a patch merged upstream to Debile's code base, and I have a prototype tool flow for analyzing a Debian package with KLEE. Roughly, this is a timeline:

    • Get more familiar with Debile's and KLEE's code bases until May 23,
    • Implement the Firehose format in KLEE until June 10,
    • Integrate KLEE into Debile until July 22,
    • Test KLEE's operation in Debile and fix glitches until the end of the GSoC program.
  • Exams and other commitments: No, I am not going to have any course exams as I passed all of them in my PhD program two years ago. Nevertheless, I am planning to have a dissertation proposal at some point during the summer.

  • Other summer plans: My summer plan is to work on this project, which perfectly aligns with my research project at the university - analyzing Debian packages with KLEE. I might take a short vacation, but I will make sure to coordinate and communicate this with GSoC project mentors.

  • Why Debian?: Debian is a free software community project. I am a strong proponent of free software. To the best of my knowledge, no other free software operating system has such a positive, big, vibrant, and independent community, not steered by any for-profit's interests. Debian as the operating system is also known for its stability. This is why I chose it to be my operating system of choice for both my laptop and servers. After being only a Debian user for 3 years, I felt like contributing back to Debian.

  • My previous Debian contributions:

    1. Two patches to Debile:
    2. A work-in-progress Debian package for the Simple Theorem Prover within the Debian Science Team (it was in the New queue once): https://anonscm.debian.org/git/debian-science/packages/stp.git

    3. A work-in-progress Debian package for KLEE: http://mentors.debian.net/package/klee

  • Are you applying for other projects in SoC? No.