research-article

Formal verification of taint-propagation security properties in a commercial SoC design

Authors:

Pramod Subramanyan,

Divya AroraAuthors Info & Claims

DATE '14: Proceedings of the conference on Design, Automation & Test in Europe

Article No.: 313, Pages 1 - 2

Published: 24 March 2014 Publication History

Get Access

Abstract

SoCs embedded in mobile phones, tablets and other smart devices come equipped with numerous features that impose specific security requirements on their hardware and firmware. Many security requirements can be formulated as taint-propagation properties that verify information flow between a set of signals in the design. In this work, we take a tablet SoC design, formulate its critical security requirements as taint-propagation properties, and prove them using a formal verification flow. We describe the properties targeted, techniques to help the verifier scale, and security bugs uncovered in the process.

References

[1]

Android Documentation: Camera.Face. https://developer.android.com/reference/android/hardware/Camera.Face.html, 2011.

Google Scholar

[2]

Google Wallet. http://www.google.com/wallet/, 2013.

Google Scholar

[3]

Widevine DRM. http://www.widevine.com/, 2013.

Google Scholar

[4]

David W. Palmer and Parbati Kumar Manna. An Efficient Algorithm for Identifying Security Relevant Logic and Vulnerabilities in RTL Designs. In Proc. of HOST, 2013.

Google Scholar

Cited By

View all

Basu KSaeed SPilato CAshraf MNabeel MChakrabarty KKarri R(2019)CAD-BaseACM Transactions on Design Automation of Electronic Systems10.1145/331557424:4(1-30)Online publication date: 18-Apr-2019
https://dl.acm.org/doi/10.1145/3315574
Huang BRay SGupta AFung JMalik S(2018)Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardwareProceedings of the 55th Annual Design Automation Conference10.1145/3195970.3196055(1-6)Online publication date: 24-Jun-2018
https://dl.acm.org/doi/10.1145/3195970.3196055
Hsieh KWang LChen WBhadra J(2017)Learning to Produce Direct Tests for Security Verification Using Constrained Process DiscoveryProceedings of the 54th Annual Design Automation Conference 201710.1145/3061639.3062271(1-6)Online publication date: 18-Jun-2017
https://dl.acm.org/doi/10.1145/3061639.3062271
Show More Cited By

Index Terms

Formal verification of taint-propagation security properties in a commercial SoC design
1. Hardware
  1. Hardware validation
    1. Functional verification
  2. Integrated circuits
    1. Interconnect

Recommendations

Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Automated Formal Verification of Application-specific Security Properties
ESSoS 2014: Proceedings of the 6th International Symposium on Engineering Secure Software and Systems - Volume 8364

In the past, formal verification of security properties of distributed applications has been mostly targeted to security protocols and generic security properties, like confidentiality and authenticity.

At ESSOS 2010, Moebius et. al. presented an ...
Formal verification of security properties of smart card embedded source code
FM'05: Proceedings of the 2005 international conference on Formal Methods

This paper reports on a method to handle the verification of various security properties of imperative source code embedded on smart cards. The idea is to combine two program verification approaches: the functional verification at the source code level ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DATE '14: Proceedings of the conference on Design, Automation & Test in Europe

March 2014

1959 pages

ISBN:9783981537024

General Chairs:
Gerhard Fettweis
TU Dresden, DE
,
Wolfgang Nebel
OFFIS, DE

In-Cooperation

SIGDA: ACM Special Interest Group on Design Automation

Publisher

European Design and Automation Association

Leuven, Belgium

Publication History

Published: 24 March 2014

Check for updates

Qualifiers

Research-article

Conference

DATE '14

Sponsor:

EDAA
EDAC
The Russian Academy of Sciences

DATE '14: Design, Automation and Test in Europe

March 24 - 28, 2014

Dresden, Germany

Acceptance Rates

Overall Acceptance Rate 518 of 1,794 submissions, 29%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
138
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)1

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Basu KSaeed SPilato CAshraf MNabeel MChakrabarty KKarri R(2019)CAD-BaseACM Transactions on Design Automation of Electronic Systems10.1145/331557424:4(1-30)Online publication date: 18-Apr-2019
https://dl.acm.org/doi/10.1145/3315574
Huang BRay SGupta AFung JMalik S(2018)Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardwareProceedings of the 55th Annual Design Automation Conference10.1145/3195970.3196055(1-6)Online publication date: 24-Jun-2018
https://dl.acm.org/doi/10.1145/3195970.3196055
Hsieh KWang LChen WBhadra J(2017)Learning to Produce Direct Tests for Security Verification Using Constrained Process DiscoveryProceedings of the 54th Annual Design Automation Conference 201710.1145/3061639.3062271(1-6)Online publication date: 18-Jun-2017
https://dl.acm.org/doi/10.1145/3061639.3062271
Li J(2017)A synthetic research on the multimedia data encryption based mobile computing security enhancement model and multi-channel mobile human computer interaction frameworkMultimedia Tools and Applications10.1007/s11042-016-3662-176:16(16963-16987)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s11042-016-3662-1
Malik SSubramanyan P(2016)Invited - Specification and modeling for systems-on-chip security verificationProceedings of the 53rd Annual Design Automation Conference10.1145/2897937.2911991(1-6)Online publication date: 5-Jun-2016
https://dl.acm.org/doi/10.1145/2897937.2911991
Subramanyan PVizel YRay SMalik SKaivola RWahl T(2015)Template-based synthesis of instruction-level abstractions for SoC verificationProceedings of the 15th Conference on Formal Methods in Computer-Aided Design10.5555/2893529.2893557(160-167)Online publication date: 27-Sep-2015
https://dl.acm.org/doi/10.5555/2893529.2893557
Rajendran JVedula VKarri R(2015)Detecting malicious modifications of data in third-party intellectual property coresProceedings of the 52nd Annual Design Automation Conference10.1145/2744769.2744823(1-6)Online publication date: 7-Jun-2015
https://dl.acm.org/doi/10.1145/2744769.2744823

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Formal verification of ASMs using MDGs

Automated Formal Verification of Application-specific Security Properties

Formal verification of security properties of smart card embedded source code