Nestan
Dr. Nestan Tsiskaridze
Home
Publications and Talks
Contact

Assistant Project Scientist

  • Since July 2016, I work in the Department of Computer Science at the University of California Santa Barbara. I have been working on the DARPA Integrated Symbolic Execution for Space-Time Analysis of Code (ISSTAC) Project. I was in the Verification Lab and my research within the project concerned with developing symbolic analysis techniques and tools for automatic identification of side-channel attacks and denial-of-service attacks in Java bytecode. I am currently working on the analysis of cryptographic codes, and quantifying information leakage in software and hardware systems, with the focus on integrating Satisfiability Modulo Theories (SMT) and leveraging further the power of automated techniques for security analysis. Since July 2018, I have moved to the Computer Architecture Lab and continue working on integrating SMT techniques in the security analysis of hardware design.

    Research Interests:

    My research interests are in developing and utilizing formal verification techniques for automating symbolic security analysis. A good and brief description of what my interests focus on are presented in my talk at Enigma 2017 -- Conference on Emerging Threats and Novel Attacks.

    Topics of Interest:
    Automated Reasoning and Verification, Decision Procedures, Model Checking.
    Satisfiability Modulo Theories (SMT), Propositional Satisfiability (SAT), Constraint Programming.
    Security Analysis, Cryptography, Program Analysis, Information Flow and Leakage.
  • Before coming to Santa Barbara I was a postdoctoral research scholar and a visiting assistant professor at the University of Iowa in the Department of Computer Science.
    I was working in Prof. Cesare Tinelli's group on developing new Satisfiability Modulo Theories (SMT) solving techniques to aid checking of software security properties, and on enhancing the CVC4 SMT solver with the new techniques. Namely, we worked on automating security analysis of Web applications and utilizing SMT techniques for this. We made CVC4 the first SMT solver capable to support the analysis of string manipulating constraints by extending CVC4 with the theory of Strings.

    During the three years at the University of Iowa I was also teaching at the Department of Computer Science:
    Computer Security -- Spring 2016, Spring 2015, Spring 2014.
    Theory of Computation -- Spring 2016, Fall 2014, Fall 2013.
    Logic in Computer Science -- Fall 2015.

    These were advanced level courses with a mixed graduate and undergraduate student enrollment. The course in Computer Security included a software security section in which CVC4, enhanced with the String support, was used by students for program analysis.
  • Before Iowa, I was a postdoctoral research associate at Princeton University in the Department of Electrical Engineering in the group of Prof. Sharad Malik.
    I was working on the DARPA Integrity and Reliability of Integrated Circuits (IRIS) Project, which concerned with reverse engineering of digital, analog and mixed-signal integrated circuits (IC) to determine their integrity and reliability for use in sensitive applications. The work involved developement of a series of algorithms for automated reverse engineering of ICs, starting from an unstructured netlist and resulting in a high-level netlist with compound components. My later work at Princeton concerned solving the All-SAT problem using minimal blocking clauses.
  • I obtained my PhD in Computer Science from the University of Manchester at the Department of Computer Science under the supervision of Prof. Andrei Voronkov.
    My PhD research was related to the development of new methods for solving SMT problems with theories of linear real and integer arithmetics. The research introduced the Conflict Driven Clause Learning-like procedures into the area of Linear Programming. The thesis presented a new method for Linear Programming - the Conflict Resolution method. The work has won two awards:
    The Best PhD Paper Award 2009 at the School of Computer Science at the University of Manchester.
    A Runner-Up as the Best Paper Prize at the CP 2009 Conference.