• National Science Foundation Computing and Communications Foundations -- Scalable Parallelism in the Extreme (SPX) (2018-2022)
  • Florida Cybersecurity Center Collaborative Seed Award (2018-2019)
  • Best Paper Award at the 10th International Conference on Foundations of Privacy & Security FPS (2017)
  • UCF Predictive Analytics Innovation Fellow (2017-2018)
  • Air Force Office of Scientific Research Young Investigator Award (2016-2019)
  • UCF Faculty Senate (2016-2017)
  • National Science Foundation Computing and Communications Foundations -- Exploiting Parallelism & Scalability (2014-2017)
  • National Science Foundation Computing and Communications Foundations -- Software & Hardware Foundations (2014-2018)
  • Best Paper Award at IEEE International Conference on Computational Advances in Bio and Medical Sciences ICCABS (2014)
  • ASE/Air Force Summer Faculty Fellowship (2014)
  • Charles N. Millican Faculty Fellow (2013)
  • IEEE Orlando Outstanding Engineering Educator Award (2013)
  • Air Force Information Directorate Visiting Faculty Fellowship Program (2013)
  • Best Paper Award at IEEE International Conference on Computational Advances in Bio and Medical Sciences ICCABS (2011)

Recent Publications

S. Jha, S. Raj, S. K. Jha, and N. Shankar, “ Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems ,” in 16th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS), Beijing, China, 2018.Abstract


We propose an automatic synthesis technique to generate provably correct controllers of stochastic linear dynamical systems for Signal Temporal Logic (STL) specifications. While formal synthesis problems can be directly formulated as exists-forall constraints, the quantifier alternation restricts the scalability of such an approach. We use the duality between a system and its proof of correctness to partially alleviate this challenge. We decompose the controller synthesis into two subproblems, each addressing orthogonal concerns - stabilization with respect to the noise, and meeting the STL specification. The overall controller is a nested controller comprising of the feedback controller for noise cancellation and an open loop controller for STL satisfaction. The correct-by-construction compositional synthesis of this nested controller relies on using the guarantees of the feedback controller instead of the controller itself. We use a linear feedback controller as the stabilizing controller for linear systems with bounded additive noise and over-approximate its ellipsoid stability guarantee with a polytope. We then use this over-approximation to formulate a mixed-integer linear programming problem (MILP) to synthesize an open-loop controller that satisfies STL specifications. We demonstrate the effectiveness of the proposed technique on a set of case studies.


S. Fernandes, S. Raj, E. Ortiz, I. Vintila, and S. K. Jha, “ Directed Adversarial Attacks on Fingerprints using Attributions ,” in International Conference on Biometrics, 2019.Abstract


Fingerprint recognition systems verify the identity of individuals and provide access to secure information in various commercial applications. However, with advancements in artificial intelligence, fingerprint-based security methods are vulnerable to attack. Such a breach has the potential to compromise confidential, private and valuable information. In this paper, we attack a state-of- the-art fingerprint recognition system based on transfer learning. Our approach uses attribution analysis to identify the fingerprint region crucial to correct classification, and then perturbs the fingerprint using error masks derived from a neural network to generate an adversarial fingerprint.

Image quality assessment metrics applied to calculate the difference between the original and perturbed fingerprints include average difference, maximum difference, normalized absolute error, and peak signal to noise ratio. On the ATVS fingerprint dataset, the differences between these values in the original and corresponding perturbed fingerprint images are negligible. Further, the VeriFinger SDK is used to detect the minutiae and perform matching between the original and perturbed fingerprints. The matching score is above 250, which reinforces the fact that there is virtually no loss between the original and perturbed fingerprints.


S. Raj, S. K. Jha, L. L. Pullum, and A. Ramanathan, “ SATYA: Defending against Adversarial Attacks using Statistical Hypothesis Testing ,” in The 10th International Symposium on Foundations and Practice of Security (FPS 2017), Nancy, France. (BEST PAPER AWARD), 2017.Abstract

The paper presents a new defense against adversarial attacks for deep neural networks. We demonstrate the effectiveness of our approach against the popular adversarial image generation method DeepFool. Our approach uses Wald's Sequential Probability Ratio Test to sufficiently sample a carefully chosen neighborhood around an input image to determine the correct label of the image. On a benchmark of 50,000 randomly chosen adversarial images generated by DeepFool we demonstrate that our method SATYA is able to recover the correct labels for 95.76% of the images for CaffeNet and 97.43% of the correct label for GoogLeNet. 


D. Chakraborty, S. Raj, J. C. Gutierrez, T. Thomas, and S. K. Jha, “ In-Memory Execution of Compute Kernels using Flow-based Memristive Crossbar Computing ,” in IEEE International Conference on Rebooting Computing 2017, Washington D.C., 2017.Abstract


Rebooting computing using in-memory architectures relies on the ability of emerging devices to execute a legacy software stack. In this paper, we present our approach of executing compute kernels written in a subset of the C pro- gramming language using flow-based computing on nanoscale memristor crossbars. Our framework also tests the correctness of the design using the parallel Xyces electronic simulation software. We demonstrate the potential of our design methodology by designing and testing a compute kernel for edge detection in images. 


A. Velasquez and S. K. Jha, “ 3D Crosspoint Memory as a Parallel Architecture for Computing Network Reachability ,” in IEEE International Conference on Computer Design (ICCD), 2018.Abstract

We introduce a new in-memory computing design that can compute single-source reachability and transitive closure of graphs by using the natural parallel flow of information in three-dimensional crosspoint memories. The proposed design can be implemented using 3D crosspoint architectures with two layers of 1-diode 1-resistor (1D1R) interconnects. Our logic-in-memory design mitigates the infamous memory-processor bottleneck characteristic of John von Neumann architectures and has a runtime complexity of $\mathcal{O}(n)$ using $\mathcal{O}(n^2)$ devices for a graph with $n$ nodes. This compares favorably to efficient algorithms on John von Neumann architectures with a time complexity of $\mathcal{O}(n^3/p + n^2 \log p)$ on $p$ processors and a competing in-memory approach with runtime $\mathcal{O}(n^2)$ using $\mathcal{O}(n^3)$ components.

S. Raj, A. Ramanathan, L. L. Pullum, and S. K. Jha, “ Testing Autonomous Cyber-Physical Systems using Fuzzing Features Derived from Convolutional Neural Networks ,” in ACM SIGBED International Conference on Embedded Software (EMSOFT), Seoul, South Korea, 2017.Abstract


Autonomous cyber-physical systems rely on modern machine learning methods such as deep neural networks to control their interactions with the physical world. Testing of such intelligent cyber-physical systems is a challenge due to the huge state space associated with high-resolution visual sensory inputs. In this paper, we demonstrate how fuzzing the input using patterns obtained from the convolutional lters of an unrelated convolutional neural network can be used to test the correctness of vision algorithms implemented in intelligent cyber-physical systems. Our method discovers interesting counterexamples to the pedestrian detection algorithm implemented in the popular OpenCV library. Our approach also unearths counterexamples to the correct behavior of an autonomous car similar to NVIDIA’s end-to-end self-driving deep neural net running on the Udacity open-source simulator.