• 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, M. Ozdag, and S. K. Jha, “ DeepAttack: Perturbation of Discriminative Fingerprint Image Region Determined by CNN ,” in International Conference on Biometrics, Forthcoming.Abstract

Fingerprints are widely used for personal identification due to their singularity and immutability. Fingerprint recognition systems verify the identity of individuals and provide access to highly-secure personal information in various commercial applications. However, with modern advancements in deep learning, fingerprint recognition systems could be attacked, rendering the personal information contained within in a highly vulnerable state. In this paper, we propose a novel approach to attack a transfer learning-based fingerprint recognition system, which is pre-trained on the ImageNet database. For experimental analysis, twelve image recognition models are considered: MobileNetV2, MobileNet, NASNetMobile, DenseNet121, DenseNet169, DenseNet201, Xception, InceptionV3, ResNet50, NASNetLarge, VGG16, and VGG19. Among them, MobileNetV2 is the latest image recognition model, but VGG16 is one of the largest used in current state-of-the-art fingerprint recognition systems. We have attacked this system using our approach on ATVS and CASIA fingerprint datasets. The image quality difference between real and attacked fingerprints calculated using image quality assessment parameters is less than 3.36%. In addition, the core has the same pixel coordinates for real and attacked fingerprints when measured using VeriFinger SDK.

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.