• Skip to primary navigation
  • Skip to main content
SRI logo
  • About
    • Press room
  • Expertise
    • Advanced imaging systems
    • Artificial intelligence
    • Biomedical R&D services
    • Biomedical sciences
    • Computer vision
    • Cyber & formal methods
    • Education and learning
    • Innovation strategy and policy
    • National security
    • Ocean & space
    • Quantum
    • QED-C
    • Robotics, sensors & devices
    • Speech & natural language
    • Video test & measurement
  • Ventures
  • NSIC
  • Careers
  • Contact
  • 日本支社
Search
Close
Home » Archives for Natarajan Shankar
Natarajan Shankar

Natarajan Shankar

Staff Scientist, Computer Science Laboratory
Go to bio page

Publications

National security publications June 1, 2015 Conference Paper

Design and Verification for Transportation System Security

Natarajan Shankar

Cyber-security has emerged as a pressing issue for transportation systems. Studies have shown that attackers can attack modern vehicles from a variety of interfaces and gain access to the most safety-critical components. Such threats become even broader and more challenging with the emergence of vehicle-to-vehicle (V2V) and vehicle-to-infrastructure (V2I) communication technologies. Addressing the security issues in transportation systems requires comprehensive approaches that encompass considerations of security mechanisms, safety properties, resource constraints, and other related system metrics. In this work, we propose an integrated framework that combines hybrid modeling, formal verification, and automated synthesis techniques for analyzing the security and safety of transportation systems and carrying out design space exploration of both in-vehicle electronic control systems and vehicle-to-vehicle communications. We demonstrate the ideas of our framework through a case study of cooperative adaptive cruise control.

Information & computer science publications October 1, 2014

A Framework for High-Assurance Quasi-Synchronous Systems

SRI International, Natarajan Shankar

In this paper, we examine the foundations of a quasi-synchronous model of computation Our version of the quasi-synchronous model is inspired by the Robot Operating System (ROS).

Information & computer science publications September 1, 2014 Article

The Semantics of Datalog for the Evidential Tool Bus

SRI International, Natarajan Shankar

The Evidential Tool Bus (ETB) is a distributed framework for tool integration for the purpose of building and maintaining assurance cases. ETB employs Datalog as a metalanguage both for defining workflows and representing arguments. The application of Datalog in ETB differs in some significant ways from its use as a database query language. For example, in ETB Datalog predicates can be tied to external tool invocations. The operational treatment of such external calls is more expressive than the use of built-in predicates in Datalog. We outline the semantic characteristics of the variant of Datalog used in ETB and describe an abstract machine for evaluating Datalog queries.

Information & computer science publications April 1, 2014 Article

The Gradual Verifier

SRI International, Natarajan Shankar

Static verification traditionally produces yes/no answers. It either provides a proof that a piece of code meets a property, or a counterexample showing that the property can be violated. Hence, the progress of static verification is hard to measure. Unlike in testing, where coverage metrics can be used to track progress, static verification does not provide any intermediate result until the proof of correctness can be computed. This is in particular problematic because of the inevitable incompleteness of static verifiers.
To overcome this, we propose a gradual verification approach, GraVy. For a given piece of Java code, GraVy partitions the statements into those that are unreachable, or from which exceptional termination is impossible, inevitable, or possible. Further analysis can then focus on the latter case. That is, even though some statements still may terminate exceptionally, GraVy still computes a partial result. This allows us to measure the progress of static verification.We present an implementation of GraVy and evaluate it on several open source projects.

Information & computer science publications March 1, 2014 Article

Reverse Engineering Digital Circuits Using Structural and Functional Analyses

SRI International, Natarajan Shankar

Integrated circuits (ICs) are now designed and fabricated in a globalized multivendor environment making them vulnerable to malicious design changes, the insertion of hardware Trojans/malware, and intellectual property (IP) theft. Algorithmic reverse engineering of digital circuits can mitigate these concerns by enabling analysts to detect malicious hardware, verify the integrity of ICs, and detect IP violations. In this paper, we present a set of algorithms for the reverse engineering of digital circuits starting from an unstructured netlist and resulting in a high-level netlist with components such as register files, counters, adders, and subtractors. Our techniques require no manual intervention and experiments show that they determine the functionality of >45% and up to 93% of the gates in each of the test circuits that we examine. We also demonstrate that our algorithms are scalable to real designs by experimenting with a very large, highly-optimized system-on-chip (SOC) design with over 375000 combinational elements. Our inference algorithms cover 68% of the gates in this SOC. We also demonstrate that our algorithms are effective in aiding a human analyst to detect hardware Trojans in an unstructured netlist.

Information & computer science publications November 1, 2013 Conference Paper

Accountable Clouds

SRI International, Natarajan Shankar

An increasing number of organizations are migrating their critical information technology services, from healthcare to business intelligence, into public cloud computing environments. However, even if cloud technologies are continuously evolving, they still have not reached a maturity level that allows them to provide users with high assurance about the security of their data beyond existent service level agreements (SLAs). To address this limitation, we propose a suite of mechanisms that enhances cloud computing technologies with more assurance capabilities. Assurance becomes a measurable property, quantified by the volume of evidence to audit and retain in a privacy-preserving and nonrepudiable fashion. By proactively collecting potential forensic evidence, the cloud becomes more accountable, while providing its regular services. In the case of a security breach, the cloud provides the appropriate reactive security framework for validating or repudiating claims. Moreover, different levels of assurance relate to different levels of storage and privacy protection requested by users, leading to an assurance-based price model for cloud services.

Cyber & formal methods publications July 1, 2013

JBernstein: A Validity Checker for Generalized Polynomial Constraints

Natarajan Shankar

Despite substantial advances in verification technology, complexity issues with classical decision procedures for nonlinear real arithmetic are still a major obstacle for formal verification of real-world applications.

Information & computer science publications June 1, 2013 Conference Paper

WordRev: Finding Word-Level Structures in a Sea of Bit-Level Gates

SRI International, Natarajan Shankar

Systems are increasingly being constructed from off-the-shelf components acquired through a globally distributed and untrusted supply chain. Often only post-synthesis gate-level netlists or actual silicons are available for security inspection. This makes reasoning about hardware trojans particularly challenging given the enormous scale of the problem. Currently, there is no mature methodology that can provide visibility into a bit-level design in terms of high-level components to allow more comprehensive analysis. In this paper, we present a systemic way of automatically deriving word-level structures from the gate-level netlist of a digital circuit. Our framework also provides the possibility for a user to specify sequences of word-level operations and it can extract the collection of gates corresponding to those operations. We demonstrate the effectiveness of our approach on a system-on-a-chip (SoC) design consisting of approximately 400,000 IBM 12SOI cells and several open-source designs.

Cyber & formal methods publications April 1, 2013 Conference Paper

Declaratively Processing Provenance Metadata

Natarajan Shankar

We propose a simple declarative language for processing provenance metadata and evaluate it by translating filters implemented in SPADE [9], an open-source provenance collection platform.

How can we help?

Once you hit send…

We’ll match your inquiry to the person who can best help you.

Expect a response within 48 hours.

Career call to action image

Make your own mark.

Search jobs

Our work

Case studies

Publications

Timeline of innovation

Areas of expertise

Institute

Leadership

Press room

Media inquiries

Compliance

Careers

Job listings

Contact

SRI Ventures

Our locations

Headquarters

333 Ravenswood Ave
Menlo Park, CA 94025 USA

+1 (650) 859-2000

Subscribe to our newsletter


日本支社
SRI International
  • Contact us
  • Privacy Policy
  • Cookies
  • DMCA
  • Copyright © 2022 SRI International