More Web Proxy on the site http://driver.im/

research-article

Public Access

Multi-representational security analysis

Authors:

Aleksandar Milicevic,

Daniel JacksonAuthors Info & Claims

FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

Pages 181 - 192

https://doi.org/10.1145/2950290.2950356

Published: 01 November 2016 Publication History

Abstract

Security attacks often exploit flaws that are not anticipated in an abstract design, but are introduced inadvertently when high-level interactions in the design are mapped to low-level behaviors in the supporting platform. This paper proposes a multi-representational approach to security analysis, where models capturing distinct (but possibly overlapping) views of a system are automatically composed in order to enable an end-to-end analysis. This approach allows the designer to incrementally explore the impact of design decisions on security, and discover attacks that span multiple layers of the system. This paper describes Poirot, a prototype implementation of the approach, and reports on our experience on applying Poirot to detect previously unknown security flaws in publicly deployed systems.

References

[1]

M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. In CCS ’97, Proceedings of the 4th ACM Conference on Computer and Communications Security, Zurich, Switzerland, April 1-4, 1997., pages 36–47, 1997.

Digital Library

[2]

G. Bai, J. Lei, G. Meng, S. S. Venkatraman, P. Saxena, J. Sun, Y. Liu, and J. S. Dong. AUTHSCAN: automatic extraction of web authentication protocols from implementations. In 20th Annual Network and Distributed System Security Symposium, NDSS 2013, San Diego, California, USA, February 24-27, 2013, 2013.

[3]

S. Ben-David, M. Chechik, and S. Uchitel. Merging partial behaviour models with different vocabularies. In CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, pages 91–105, 2013.

Digital Library

[4]

A. Biere. Lingeling essentials, A tutorial on design and implementation aspects of the the SAT solver lingeling. In POS-14. Fifth Pragmatics of SAT workshop, a workshop of the SAT 2014 conference, part of FLoC 2014 during the Vienna Summer of Logic, July 13, 2014, Vienna, Austria, page 88, 2014.

[5]

B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada, pages 82–96, 2001.

Digital Library

[6]

G. Bruns and P. Godefroid. Model checking partial state spaces with 3-valued temporal logics. In 11th International Conference on Computer Aided Verification, CAV 1999, Italy, pages 274–287, 1999.

Digital Library

[7]

K. Z. Chen, W. He, D. Akhawe, V. D’Silva, P. Mittal, and D. Song. ASPIRE: iterative specification synthesis for security. In 15th Workshop on Hot Topics in Operating Systems, HotOS XV, Kartause Ittingen, Switzerland, May 18-20, 2015, 2015.

Digital Library

[8]

M. R. Clarkson and F. B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157–1210, 2010.

Digital Library

[9]

A. Datta, A. Derek, J. C. Mitchell, and A. Roy. Protocol composition logic (PCL). Electr. Notes Theor. Comput. Sci., 172:311–358, 2007.

Digital Library

[10]

S. M. Easterbrook and B. Nuseibeh. Managing inconsistencies in an evolving specification. In RE, pages 48–55, 1995.

Digital Library

[11]

M. Famelis, R. Salay, and M. Chechik. Partial models: Towards modeling and reasoning with uncertainty. In 34th International Conference on Software Engineering, ICSE 2012, Zurich, Switzerland, pages 573–583, 2012.

Digital Library

[12]

D. Garg, J. Franklin, D. K. Kaynar, and A. Datta. Compositional system security with interface-confined adversaries. Electr. Notes Theor. Comput. Sci., 265:49–71, 2010.

Digital Library

[13]

G. Georg, I. Ray, K. Anastasakis, B. Bordbar, M. Toahchoodee, and S. H. Houmb. An aspect-oriented methodology for designing secure applications. Information & Software Technology, 51(5):846–864, 2009.

Digital Library

[14]

C. A. R. Hoare. Communicating sequential processes. Commun. ACM, 21(8):666–677, 1978.

Digital Library

[15]

M. Huth, R. Jagadeesan, and D. A. Schmidt. Modal transition systems: A foundation for three-valued program analysis. In 10th European Symposium on Programming Languages and Systems, ESOP 2001, Genova, Italy, pages 155–169, 2001.

Digital Library

[16]

Internet Engineering Task Force. OAuth Authorization Framework. http://tools.ietf.org/html/rfc6749, 2014.

[17]

D. Jackson. Structuring Z specifications with views. ACM Trans. Softw. Eng. Methodol., 4(4):365–389, 1995.

Digital Library

[18]

D. Jackson. Software Abstractions: Logic, language, and analysis. MIT Press, 2006.

Digital Library

[19]

A. Judson. Tamper data plugin for firefox. https:// addons.mozilla.org/en-us/firefox/addon/tamper-data. Accessed: 2015-03-15.

[20]

E. Kang. Multi-Representational Security Modeling and Analysis. PhD thesis, MIT, 2016.

[21]

O. Kupferman, M. Y. Vardi, and P. Wolper. Module checking. Information and Computation, 164(2):322–344, 2001.

Digital Library

[22]

B. W. Lampson. A note on the confinement problem. Commun. ACM, 16(10):613–615, 1973.

Digital Library

[23]

H. C. Li, S. Krishnamurthi, and K. Fisler. Verifying cross-cutting features as open systems. In 10th Symposium on Foundations of Software Engineering, South Carolina, USA, pages 89–98, 2002.

Digital Library

[24]

G. Lowe. Casper: A compiler for the analysis of security protocols. In 10th Computer Security Foundations Workshop (CSFW ’97), June 10-12, 1997, Rockport, Massachusetts, USA, pages 18–30, 1997.

Digital Library

[25]

H. Mantel. On the composition of secure systems. In 2002 IEEE Symposium on Security and Privacy, Berkeley, California, USA, May 12-15, 2002, pages 88–101, 2002.

Digital Library

[26]

S. Maoz, J. O. Ringert, and B. Rumpe. Synthesis of component and connector models from crosscutting structural views. In ESEC/FSE’13, Saint Petersburg, Russian Federation, August 18-26, 2013, pages 444–454, 2013.

Digital Library

[27]

A. Milicevic, J. P. Near, E. Kang, and D. Jackson. Alloy*: A general-purpose higher-order relational constraint solver. In 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Volume 1, pages 609–619, 2015.

Digital Library

[28]

Mitre. Common Attack Pattern Enumeration and Classification. http://capec.mitre.org, 2014.

[29]

S. Nejati, M. Sabetzadeh, M. Chechik, S. M. Easterbrook, and P. Zave. Matching and merging of statecharts specifications. In ICSE, pages 54–64, 2007.

Digital Library

[30]

B. Nuseibeh, J. Kramer, and A. Finkelstein. Expressing the relationships between multiple views in requirements specification. In ICSE, pages 187–196, 1993.

Digital Library

[31]

Open Web Application Security Project. OWASP Top Ten Project. http://www.owasp.org/index.php, 2014.

[32]

R. Pottinger and P. A. Bernstein. Merging models based on given correspondences. In VLDB, pages 826–873, 2003.

Digital Library

[33]

P. Y. A. Ryan and S. A. Schneider. Modelling and analysis of security protocols. Addison-Wesley-Longman, 2001.

Digital Library

[34]

M. Sabetzadeh and S. M. Easterbrook. An algebraic framework for merging incomplete and inconsistent views. In RE, pages 306–318, 2005.

Digital Library

[35]

A. Solar-Lezama, L. Tancau, R. Bod´ık, S. A. Seshia, and V. A. Saraswat. Combinatorial sketching for finite programs. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, San Jose, CA, USA, October 21-25, 2006, pages 404–415, 2006.

Digital Library

[36]

F. J. Thayer, J. C. Herzog, and J. D. Guttman. Strand spaces: Why is a security protocol correct? In 1998 IEEE Symposium on Security and Privacy, Oakland, CA, USA, May 3-6, 1998, Proceedings, pages 160–171, 1998.

[37]

S. Uchitel and M. Chechik. Merging partial behavioural models. In SIGSOFT FSE, pages 43–52, 2004.

Digital Library

Cited By

Cámara J(2024)Exploring the interaction of design variability and stochastic operational uncertainties in software-intensive systems through the lens of modelingSoftware and Systems Modeling10.1007/s10270-024-01226-5Online publication date: 11-Nov-2024
https://doi.org/10.1007/s10270-024-01226-5
Chen HZhou SChen CDai ZLi B(2023)A Business-Oriented Methodology to Evaluate the Security of Software Architecture QuantitativelyInternational Journal of Software Engineering and Knowledge Engineering10.1142/S021819402350051134:02(239-271)Online publication date: 26-Sep-2023
https://doi.org/10.1142/S0218194023500511
Matsui SLafortune S(2022)Synthesis of winning attacks on communication protocols using supervisory control theory: two case studiesDiscrete Event Dynamic Systems10.1007/s10626-022-00369-132:4(573-610)Online publication date: 20-Oct-2022
https://doi.org/10.1007/s10626-022-00369-1
Show More Cited By

Index Terms

Multi-representational security analysis
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

Threat-Driven Modeling and Verification of Secure Software Using Aspect-Oriented Petri Nets

Design-level vulnerabilities are a major source of security risks in software. To improve trustworthiness of software design, this paper presents a formal threat-driven approach, which explores explicit behaviors of security threats as the mediator ...
Risk-based design security analysis
SEAD '18: Proceedings of the 1st International Workshop on Security Awareness from Design to Deployment

Implementing security by design in practice often involves the application of threat modeling to elicit security threats and to aid designers in focusing efforts on the most stringent problems first.

Existing threat modeling methodologies are capable of ...
Security and Integrity Analysis Using Indicators
CYBERSECURITY '12: Proceedings of the 2012 International Conference on Cyber Security

Computer systems today are under constant attack by adversaries that are looking for opportunistic ways to gain access and exfiltrate data, cause disruption or chaos, or leverage the computer for their own use. Whatever the motives are, these attacks ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

November 2016

1156 pages

ISBN:9781450342186

DOI:10.1145/2950290

General Chair:
Thomas Zimmermann
Microsoft Research, USA
,
Program Chairs:
Jane Cleland-Huang
University of Notre Dame, USA
,
Zhendong Su
University of California at Davis, USA

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

NSF

Conference

FSE'16

Sponsor:

SIGSOFT

FSE'16: 24nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering

November 13 - 18, 2016

WA, Seattle, USA

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
485
Total Downloads

Downloads (Last 12 months)63
Downloads (Last 6 weeks)5

Reflects downloads up to 03 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Cámara J(2024)Exploring the interaction of design variability and stochastic operational uncertainties in software-intensive systems through the lens of modelingSoftware and Systems Modeling10.1007/s10270-024-01226-5Online publication date: 11-Nov-2024
https://doi.org/10.1007/s10270-024-01226-5
Chen HZhou SChen CDai ZLi B(2023)A Business-Oriented Methodology to Evaluate the Security of Software Architecture QuantitativelyInternational Journal of Software Engineering and Knowledge Engineering10.1142/S021819402350051134:02(239-271)Online publication date: 26-Sep-2023
https://doi.org/10.1142/S0218194023500511
Matsui SLafortune S(2022)Synthesis of winning attacks on communication protocols using supervisory control theory: two case studiesDiscrete Event Dynamic Systems10.1007/s10626-022-00369-132:4(573-610)Online publication date: 20-Oct-2022
https://doi.org/10.1007/s10626-022-00369-1
Zhang CWagner ROrvalho PGarlan DManquinho VMartins RKang ESpinellis DGousios GChechik MDi Penta M(2021)AlloyMax: bringing maximum satisfaction to relational specificationsProceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3468264.3468587(155-167)Online publication date: 20-Aug-2021
https://dl.acm.org/doi/10.1145/3468264.3468587
Cámara J(2020)HaiQProceedings of the 8th International Conference on Formal Methods in Software Engineering10.1145/3372020.3391562(22-33)Online publication date: 7-Oct-2020
https://dl.acm.org/doi/10.1145/3372020.3391562
Kang ELafortune STripakis S(2019)Automated Synthesis of Secure Platform MappingsComputer Aided Verification10.1007/978-3-030-25540-4_12(219-237)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25540-4_12
Bastys IBalliu MSabelfeld ALie DMannan MBackes MWang X(2018)If This Then What?Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security10.1145/3243734.3243841(1102-1119)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.1145/3243734.3243841
Wang KSullivan AKoukoutos MMarinov DKhurshid S(2018)Systematic Generation of Non-equivalent Expressions for Relational AlgebraAbstract State Machines, Alloy, B, TLA, VDM, and Z10.1007/978-3-319-91271-4_8(105-120)Online publication date: 8-May-2018
https://doi.org/10.1007/978-3-319-91271-4_8
Cámara JGarlan DSchmerl B(2017)Synthesis and Quantitative Verification of Tradeoff Spaces for Families of Software SystemsSoftware Architecture10.1007/978-3-319-65831-5_1(3-21)Online publication date: 15-Aug-2017
https://doi.org/10.1007/978-3-319-65831-5_1
Kang E(2016)Design Space Exploration for Security2016 IEEE Cybersecurity Development (SecDev)10.1109/SecDev.2016.017(30-36)Online publication date: Nov-2016
https://doi.org/10.1109/SecDev.2016.017

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents