publications

2025

1. Checking δ-Satisfiability of Reals with Integrals

   Cody Rivera, Bishnu Bhusal, Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan

   Proc. ACM Program. Lang., Apr 2025

   Abs

   Many synthesis and verification problems can be reduced to determining the truth of formulas over the real numbers. These formulas often involve constraints with integrals in them. To this end, we extend the framework of δ-decision procedures with techniques for handling integrals of user-specified real functions. We implement this decision procedure in the tool ∫dReal, which is built on top of dReal. We evaluate ∫dReal on a suite of problems that include formulas verifying the fairness of algorithms and the privacy and the utility of privacy mechanisms and formulas that synthesize parameters for the desired utility of privacy mechanisms. The performance of the tool in these experiments demonstrates the effectiveness of ∫dReal.

2. Privacy Nutrition Labels: Promise, Practice, and Paradoxes in Communicating Privacy

   Bishnu Bhusal, Yuanye Ma, and Rohit Chadha

   In HCI International 2025 Posters , Apr 2025

   PDF
3. Cyber AI Trends

   Mir Mehedi Rahman, Sazzad Hossain, Bishnu Bhusal, and Naresh Kshetri

   In Advances in Social Networking and Online Communities , Feb 2025

   Abs

   Generative Artificial Intelligence (AI) is opening new paths in the detection and prevention of cyberbullying. As we know, AI is shaping and improving the future of cyber, industry, automation, manufacturing, healthcare etc. with challenges of privacy concerns, job losses issues, and increased rules. This chapter explores future trends in AI-driven tools designed to reduce online bullying including various cybercrime across social media platforms, messaging apps, and other digital platforms. Ethical concerns like security and privacy, fairness, and avoiding bias are also discussed, aiming to ensure that AI tools are used responsibly and transparently. By combining technical advancements with an understanding of social impact, this chapter presents a vision for AI systems that create safer, more supportive online spaces. The chapter highlights the potential of generative AI to shape digital environments that are inclusive, resilient, and protective, fostering healthier interactions for everyone involved with the future scope of the study.

2024

1. Formal Verification for Blockchain-based Insurance Claims Processing

   Roshan Lal Neupane, Ernest Bonnah, Bishnu Bhusal, Kiran Neupane, Khaza Anuarul Hoque, and Prasad Calyam

   Feb 2024
2. On Countering Ransomware Attacks Using Strategic Deception

   Roshan Lal Neupane, Bishnu Bhusal, Kiran Neupane, Preyea Regmi, Tam Dinh, Lilliana Marrero, Sayed M. Saghaian N. E., Venkata Sriram Siddhardh Nadendla, and Prasad Calyam

   In Decision and Game Theory for Security , Feb 2024

   Abs

   Ransomware attacks continue to be a major concern for critical systems that are vital for society e.g., healthcare, finance, and transportation. Traditional cyber defense mechanisms fail to pose dynamic measures to stop ransomware attacks from progressing through various stages in the attack process. To this end, intelligent cyber deception strategies can be effective when they leverage information about attacker strategies and deploy deceptive assets to increase the cost or complexity of a successful exploit or discourage continued attacker efforts. In this paper, we present a novel game theoretic approach that uses deception-based defense strategies at each of the ransomware attack stages for optimization of the decision-making to outsmart attacker advances. Specifically, we propose a multistage ransomware game model that deploys a combination of deception assets i.e., honeytokens, honeypots, honeyfiles, and network honeypots in subgames. Using closed-form backward induction, we evaluated Subgame-Perfect Nash Equilibrium (SPNE). We perform a numerical analysis using real-world data and statistics pertaining to the impact of ransomware attacks in the healthcare sector. Our healthcare case study evaluation results show that the use of deception technologies is favorable to the defender. This work elucidates the profound implications of strategic deception in cybersecurity, demonstrating its capacity to complicate successful exploits and consequently bolster the defense of key societal infrastructures.

3. blockDADS: Blockchain Technology for Data Analytics and Data Security - Applications and Solutions

   Omar Faruq Osama, Bishnu Bhusal, Naresh Kshetri, and Bishwo Prakash Pokharel

   In Blockchain Technology for Cyber Defense, Cyber Security, and Countermeasures: Techniques, Solutions, and Applications , Feb 2024

2023

1. VTON-IT: Virtual Try-On using Image Translation

   Santosh Adhikari, Bishnu Bhusal, Prashant Ghimire, and Anil Shrestha

   Feb 2023
2. Deciding Differential Privacy of Online Algorithms with Multiple Variables

   Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan, and Bishnu Bhusal

   In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security , , Copenhagen, Denmark, , Feb 2023

   Abs

   We consider the problem of checking the differential privacy of online randomized algorithms that process a stream of inputs and produce outputs corresponding to each input. This paper generalizes an automaton model called DiP automata [10] to describe such algorithms by allowing multiple real-valued storage variables. A DiP automaton is a parametric automaton whose behavior depends on the privacy budget ∈. An automaton A will be said to be differentially private if, for some D, the automaton is D∈-differentially private for all values of ∈ > 0. We identify a precise characterization of the class of all differentially private DiP automata. We show that the problem of determining if a given DiP automaton belongs to this class is PSPACE-complete. Our PSPACE algorithm also computes a value for D when the given automaton is differentially private. The algorithm has been implemented, and experiments demonstrating its effectiveness are presented.