abdulbaki aydın

abakiaydinn [at] gmail [.] com

Now, graduated...


I am a member of Verification Lab where I am being advised by Prof. Tevfik Bultan.

I recently work on designing and implementing algorithms and building tools for software side channel analysis as part of the project that is funded by The Space/Time Analysis for Cybersecurity (STAC) program of DARPA. My current work spans research topics such as model counting, constraint solving, symbolic execution, and software security. Previously, I worked on analysis of web applications (JS, PHP) using automata based symbolic string execution techniques to automatically find and fix security related vulnerabilities. I worked on privacy threat detection and prevention on mobile platforms using dynamic analysis techniques (Android).

Other than research and development, I enjoy playing soccer, surfing (need more practice), traveling around, and exploring new places with my wife Yasemin.

Learn about my research interests

My Research Interests

to improve software dependability, software security, and developer productivity.

Model Counting and Constraint Solving

for vulnerability analysis on modern applications

Program Analysis (Static/Dynamic)

software side channel analysis, string analysis, complexity analysis

Automated Verification and Testing

bug discovery/fixing, test case generation, software security

Programming Languages and Compilers

optimizations, execution environments, domain specific languages

Books

  • String Analysis for Software Verification and Security

    Tevfik Bultan, Fang Yu, Muath Alkhalaf, Abdulbaki Aydin

    Springer 2017, ISBN 978-3-319-68668-4, pp. 1-166 (e-book)

Publications

  • Parameterized Model Counting for String and Numeric Constraints (Project Web Page)

    Abdulbaki Aydin, William Eiers, Lucas Bang, Tegan Brennan, Miroslav Gavrilov, Tevfik Bultan, Fang Yu

    To be appear in The 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2018).

  • Constraint normalization and parameterized caching for quantitative program analysis

    Tegan Brennan, Nestan Tsiskaridze, Nicolás Rosner, Abdulbaki Aydin, Tevfik Bultan

    Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2017).

  • Visual Configuration of Mobile Privacy Policies

    Abdulbaki Aydin, David Piorkowski, Omer Tripp, Pietro Ferrara, Marco Pistoia

    To be appear in The 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017).

  • String Analysis for Side Channels with Segmented Oracles

    Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Pasareanu, Tevfik Bultan

    The 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2016), Seattle, Washington, USA, November 13-18, 2016.

  • Automata-based Model Counting for String Constraints (Project Web Page)

    Abdulbaki Aydin, Lucas Bang, Tevfik Bultan

    Proceedings of the 27th International Conference on Computer Aided Verification, Part 1 (CAV 2015), pages 255-272, San Francisco, California, USA, July 18-24, 2015.

  • Automatically Computing Path Complexity of Programs (Online Demo - Project Web Page)

    Lucas Bang, Abdulbaki Aydin, Tevfik Bultan

    Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2015), pages 61-72, Bergamo, Italy, Sep 02-04, 2015.

  • Semantic Differential Repair for Input Validation and Sanitization (Project Web Page)

    Muath Alkhalaf, Abdulbaki Aydin, Tevfik Bultan

    Proceedings of the 2014 International Symposium on Software Testing and Analysis (ISSTA 2014), pages 225-236, San Jose, California, USA, July 21-25, 2014.

  • Automated Test Generation from Vulnerability Signatures

    Abdulbaki Aydin, Muath Alkhalaf, Tevfik Bultan

    Proceedings of the 7th International Conference on Software Testing, Verification and Validation (ICST 2014), pages 193-202, Cleveland, Ohio, USA, March 31-April 4, 2014.

Tutorials

  • String Analysis for Vulnerability Detection and Repair

    Tevfik Bultan, Abdulbaki Aydin, Lucas Bang

    The 37th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI 2016), Santa Barbara, CA, USA, June 13-17, 2016.

Workshops

  • Automated Test Generation from Vulnerability Signatures *Best paper award receiver

    Abdulbaki Aydin, Muath Alkhalaf, Tevfik Bultan

    Graduate Student Workshop (GSWC 2014), Santa Barbara, CA, USA, Oct 10, 2014.

Projects and Tools

ABC
Automata Based model Counter

ABC is an automata-based model counting constraint solver. It is the only model counter that supports string theory and linear integer arithmetic theory simultaneously. ABC has many applications, including but not limited to, probabilistic symbolic execution, quantitative information flow analysis, test case generation, automated repair, vulnerability analysis, string analysis. Please see our CAV'15 publication for theoritical details. Currently, we are writing a paper on improvements and additions to ABC.

PAC
PAth Complexity analyzer

PAC analyzes your code and extracts a theoretical bound on worst case path complexity of your code. There is an online demo available!. PAC currently supports analysis of Java programs and can be extended to any programming language. Please see our ESEC/FSE'15 publication for theoretical details. We are working on improving PAC with inter-procedural analysis.

SemRep
Semantic Differential Repair

SemRep analyzes and repairs validation and sanitization functions against each other. The tool does not need any manual specification or intervention. It takes two functions as Dependency Graphs then it looks for differences in validation and sanitization operations for string variables. If a difference is found, the tool suggests a set of three patch functions that can be used to fix the difference. Please see our ISSTA'14 publication for theoretical details.

Resume

Download

baki [at] cs [.] ucsb [.] edu

Find me on ...