I am 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 interests lie at the intersection of networked systems and security. Broadly, I'm interested in tackling practical cybersecurity problems in the networking domain, where the overarching goal is to create automated techniques to achieve higher assurance on networked systems. I primarily apply program analysis and formal verification techniques to design and develop automated analysis techniques for aiding the development of secure networked systems, including real-world implementations of network protocols and IoT systems.
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!