I’m a recent Master’s graduate from Carnegie Mellon University. Prior to CMU, I worked at Microsoft Research India as a Research Fellow in the Programming Languages and Software Engineering group. I obtained my bachelor’s degree in Computer Science and Engineering from National Institute of Technology Karnataka in India.

My research interests include using formal verification and other automated reasoning techniques to improve software and system security. During my Master’s, I worked with Bryan Parno on applying these techniques to formally verify the security of cryptographic protocols. My work at CertiK and MSR also focused on using these techniques to verify blockchain smart contracts. I am also interested in program analysis, programming language theory and compilers.

When I’m not working, I play a lot of chess. (Fun fact: I got to meet and play with Magnus Carlsen a couple of years ago!) I also like to read fiction, play the guitar and draw.

Update: I am currently on the job market and am looking for full-time opportunities. Please reach out to me if you or somebody you know are hiring!

Experience

Publications

• Owl: Compositional Verification of Security Protocols via an Information-Flow Type System

  IEEE S&P 2023, March 2023

  Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, Bryan Parno

   Paper    Abstract

  Computationally sound protocol verification tools promise to deliver full-strength cryptographic proofs for security protocols. Unfortunately, current tools lack either modularity or automation. We propose a new approach based on a novel use of information flow and refinement types for sound cryptographic proofs. Our framework, Owl, allows type-based modular descriptions of security protocols, wherein disjoint subprotocols can be programmed and automatically proved secure separately. We give a formal security proof for Owl via a core language which supports standard symmetric and asymmetric primitives, Diffie-Hellman operations, and hashing via random oracles. We also implement a type checker for Owl along with a prototype extraction mechanism to Rust, and evaluate it on 14 case studies, including (simplified forms of) SSH key exchange and Kerberos.

  
  
• Celestial: A Smart Contracts Verification Framework

  FMCAD 2021, October 2021

  Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi, Akash Lal

   Paper    Abstract

  We present Celestial, a framework for formally verifying smart contracts written in the Solidity language for the Ethereum blockchain. Celestial allows programmers to write expressive functional specifications for their contracts. It translates the contracts and the specifications to F* to formally verify, against an F* model of the blockchain semantics, that the contracts meet their specifications. Once the verification succeeds, Celestial performs an erasure of the specifications to generate Solidity code for execution on the Ethereum blockchain. We use Celestial to verify several real-world smart contracts from different application domains such as tokens, digital wallets, and governance. Our experience shows that Celestial is a valuable tool for writing high-assurance smart contracts.

  
  
• Breeding Unicorns: Developing Trustworthy and Scalable Randomness Beacons

  PLOS ONE, April 2020

  Samvid Dharanikota, Rene Rydhof Hansen, Michael Jensen, Sebastian Ro Kristensen, Matthias Sass Michno, Yvonne-Anne Pignolet, Stefan Schmid

   Paper    Abstract

  Randomness beacons are services that periodically emit a random number, allowing users to agree on the same random outcome without trusting anyone: ideally, the randomness beacon is secure (cannot be influenced) and transparent (can be monitored by users). Hence, such randomness beacons can serve as an important primitive for smart contracts in a variety of contexts. In this paper we aim to bridge the gap between theory and practice of public beacon design inspired by the unicorn protocol of Lenstra and Wesolowski using verifiable delay functions. We first present a structured security analysis, based on which we design, implement, and evaluate a trustworthy and efficient randomness beacon allowing users to join at any time. We then compare different implementation and deployment options on distributed ledgers, and report on a Ethereum smart contract-based lottery using our beacon.

  
  
• CollabChain: Blockchain-Backed Trustless Web-Based Volunteer Computing Platform

  IFIP International Conference on Computer Information Systems and Industrial Management (pp. 509-522), September 2019

  Samvid Dharanikota, Sagar Bharadwaj KS, Adarsh Honawad, K. Chandrasekaran

   Paper    Abstract

  Volunteer computing is a distributed computing model in which individuals in possession of computing resources volunteer to provide them to a project. Owing to the availability of billions of computing devices all over the world, volunteer computing can help solve problems that are larger in scale even for supercomputers. However, volunteer computing projects are difficult to launch and deploy. These platforms also force volunteers to trust the authenticity of the project owner and to blindly accept credits allotted to their contribution by the project owner. As a result, very few high-profile trusted projects are able to sustain in this system. In this paper, we present an incentivized web-based volunteer computing platform that functions as a market place to buy and sell computing power. Launching a project on the system and contributing to an existing project happens over the browser without the need for a specialized software or hardware. We introduce the application of blockchain to remove the need to trust any other party in the system. We also present a prototype implementation and solve NP-Problems as examples using the proposed prototype.

  
  
• Blockchain Research and Applications: A Systematic Mapping Study

  Springer IETE International Conference on Blockchain Technology (IC-BCT 2019), March 2019

  Samvid Dharanikota, Sagar Bharadwaj KS, Adarsh Honawad, K. Chandrasekaran

   Paper    Abstract

  Brought to the limelight by the famous Bitcoin, blockchain has since evolved, and now sees a lot of use cases apart from cryptocurrencies, such as in distributed storage systems, finance, healthcare, and so on. It is, therefore, an area of scrutiny by a lot of researchers and application developers. A significant amount of research on blockchain involves the application of blockchain technology to solve problems from various domains or improve the existing architecture of blockchain itself. The recent trend towards the decentralization of the Internet has given rise to many decentralized applications which also rely fundamentally on blockchain. In this paper, we conducted a systematic mapping study on blockchain technologies. The objective of the study is to identify and map various domains of research related to blockchain and recognize possible directions for future research. We do so by formulating a set of well-defined research questions and providing answers to them.

  
  

Projects

• Verified Datalog Engine Nov 2022 - Dec 2022
• Embedded OS Sep 2022 - Dec 2022
• CollabChain Nov 2018 - Mar 2019
• Low-rate TCP Targetted DoS Attack Simulation Jan 2018 - Apr 2018