I am an Assistant Professor in the Department of Electrical Engineering and Computer Science at Syracuse University (SU). Before joining SU, I was an Assistant Professor in the School of Computing and Information Sciences at Florida International University (FIU) . I received my Ph.D. in Computer Science from from the Department of Computer Science at Purdue University under the supervision of Prof. Cristina Nita-Rotaru in 2015. During 2016, I was a Postdoctoral Research Associate at Northeastern University (Host: Prof. Cristina Nita-Rotaru).
My research focuses on security of computer networks and systems. Software of computer networks and systems continues to have exploitable vulnerabilities, which are lucrative targets for adversaries. Within this broad domain, my particular emphasis is on automated detection of vulnerabilities as well as creating resilient protocols and systems. My research primarily builds on and expands program analysis, software engineering, and formal verification. My interests span several domains of computing, including network communication protocols, operating systems, distributed systems, Internet-of-Things (IoT) systems, and embedded devices.
The X.509 Public-Key Infrastructure has long been used in the SSL/TLS protocol to achieve authentication. A recent trend of Internet-of-Things (IoT) systems employing small footprint SSL/TLS libraries for secure communication has further propelled its prominence. The security guarantees provided by X.509 hinge on the assumption that the underlying implementation rigorously scrutinizes X.509 certificate chains, and accepts only the valid ones. Noncompliant implementations of X.509 can potentially lead to attacks and/or interoperability issues. In the literature, black-box fuzzing has been used to find flaws in X.509 validation implementations; fuzzing, however, cannot guarantee coverage and thus severe flaws may remain undetected. To thoroughly analyze X.509 implementations in small footprint SSL/TLS libraries, this paper takes the complementary approach of using symbolic execution.
We observe that symbolic execution, a technique proven to be effective in finding software implementation flaws, can also be leveraged to expose noncompliance in X.509 implementations. Directly applying an off-the-shelf symbolic execution engine on SSL/TLS libraries is, however, not practical due to the problem of path explosion. To this end, we propose the use of SymCerts, which are X.509 certificate chains carefully constructed with a mixture of symbolic and concrete values. Utilizing SymCerts and some domain-specific optimizations, we symbolically execute the certificate chain validation code of each library and extract path constraints describing its accepting and rejecting certificate universes. These path constraints help us identify missing checks in different libraries. For exposing subtle but intricate noncompliance with X.509 standard, we cross-validate the constraints extracted from different libraries to find further implementation flaws. Our analysis of 9 small footprint X.509 implementations has uncovered 48 instances of noncompliance. Findings and suggestions provided by us have already been incorporated by developers into newer versions of their libraries.
The best way to contact me is through email!