A logic for secure stratified systems and its application to containerized systems

Hagen Lauer, Amin Sakzad, Carsten Rudolph, Surya Nepal

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

Abstract

We present the design and verification of a secure integrity measurement system for containerized systems. Containerization of applications allows fine-graded deployment and management of services and dependencies but also needs fine-graded security mechanisms. In this paper we provide formal abstractions for containerized systems by introducing LS^3, a formal model and logic with sub-domain constructs to represent stratified systems and their interactions. Using our formal model, we prove that the widely used Trusted Computing Group (TCG) based Integrity Measurement Architecture (IMA) securely extends trust measurements from boot to applications. However, IMA is not designed to make domain specific trust measurements and is consequently incapable of creating domain specific integrity reports. Current research aims to improve either trust measurement performance or comprehensiveness but does not improve the measurement function and its semantics to allow remote verification of measurements per domain. We present an enhanced trust measurement architecture design, which produces domain specific integrity measurements suitable for fine-graded remote attestation. Providing domain specific integrity reports eases system and sub-system verification and yields desirable properties such as measurement log stability and constrained disclosure for multi-domain systems. We verify and prove the correctness of our trust measurement architecture using our formal model.

Original languageEnglish
Title of host publicationProceedings - 2019 18th IEEE International Conference on Trust, Security and Privacy in Computing and Communications/13th IEEE International Conference on Big Data Science and Engineering
EditorsLiqun Chen, Ryan Ko, Liming Zhu
Place of PublicationPiscataway NJ USA
PublisherIEEE, Institute of Electrical and Electronics Engineers
Pages562-569
Number of pages8
ISBN (Electronic)9781728127767, 9781728127774
ISBN (Print)9781728127781
DOIs
Publication statusPublished - 2019
EventIEEE International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom) 2019 - Rotorua, New Zealand
Duration: 5 Aug 20198 Aug 2019
Conference number: 18th
https://crow.org.nz/TrustCom2019

Conference

ConferenceIEEE International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom) 2019
Abbreviated titleTrustCom 2019
CountryNew Zealand
CityRotorua
Period5/08/198/08/19
Internet address

Keywords

  • Formal Verification
  • Trusted Computing
  • Virtualization

Cite this

Lauer, H., Sakzad, A., Rudolph, C., & Nepal, S. (2019). A logic for secure stratified systems and its application to containerized systems. In L. Chen, R. Ko, & L. Zhu (Eds.), Proceedings - 2019 18th IEEE International Conference on Trust, Security and Privacy in Computing and Communications/13th IEEE International Conference on Big Data Science and Engineering (pp. 562-569). [8887372] Piscataway NJ USA: IEEE, Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/TrustCom/BigDataSE.2019.00081
Lauer, Hagen ; Sakzad, Amin ; Rudolph, Carsten ; Nepal, Surya. / A logic for secure stratified systems and its application to containerized systems. Proceedings - 2019 18th IEEE International Conference on Trust, Security and Privacy in Computing and Communications/13th IEEE International Conference on Big Data Science and Engineering. editor / Liqun Chen ; Ryan Ko ; Liming Zhu. Piscataway NJ USA : IEEE, Institute of Electrical and Electronics Engineers, 2019. pp. 562-569
@inproceedings{fd3eb27680d147f58514783ba1e4dde1,
title = "A logic for secure stratified systems and its application to containerized systems",
abstract = "We present the design and verification of a secure integrity measurement system for containerized systems. Containerization of applications allows fine-graded deployment and management of services and dependencies but also needs fine-graded security mechanisms. In this paper we provide formal abstractions for containerized systems by introducing LS^3, a formal model and logic with sub-domain constructs to represent stratified systems and their interactions. Using our formal model, we prove that the widely used Trusted Computing Group (TCG) based Integrity Measurement Architecture (IMA) securely extends trust measurements from boot to applications. However, IMA is not designed to make domain specific trust measurements and is consequently incapable of creating domain specific integrity reports. Current research aims to improve either trust measurement performance or comprehensiveness but does not improve the measurement function and its semantics to allow remote verification of measurements per domain. We present an enhanced trust measurement architecture design, which produces domain specific integrity measurements suitable for fine-graded remote attestation. Providing domain specific integrity reports eases system and sub-system verification and yields desirable properties such as measurement log stability and constrained disclosure for multi-domain systems. We verify and prove the correctness of our trust measurement architecture using our formal model.",
keywords = "Formal Verification, Trusted Computing, Virtualization",
author = "Hagen Lauer and Amin Sakzad and Carsten Rudolph and Surya Nepal",
year = "2019",
doi = "10.1109/TrustCom/BigDataSE.2019.00081",
language = "English",
isbn = "9781728127781",
pages = "562--569",
editor = "Chen, {Liqun } and Ko, {Ryan } and Zhu, {Liming }",
booktitle = "Proceedings - 2019 18th IEEE International Conference on Trust, Security and Privacy in Computing and Communications/13th IEEE International Conference on Big Data Science and Engineering",
publisher = "IEEE, Institute of Electrical and Electronics Engineers",
address = "United States of America",

}

Lauer, H, Sakzad, A, Rudolph, C & Nepal, S 2019, A logic for secure stratified systems and its application to containerized systems. in L Chen, R Ko & L Zhu (eds), Proceedings - 2019 18th IEEE International Conference on Trust, Security and Privacy in Computing and Communications/13th IEEE International Conference on Big Data Science and Engineering., 8887372, IEEE, Institute of Electrical and Electronics Engineers, Piscataway NJ USA, pp. 562-569, IEEE International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom) 2019, Rotorua, New Zealand, 5/08/19. https://doi.org/10.1109/TrustCom/BigDataSE.2019.00081

A logic for secure stratified systems and its application to containerized systems. / Lauer, Hagen; Sakzad, Amin; Rudolph, Carsten; Nepal, Surya.

Proceedings - 2019 18th IEEE International Conference on Trust, Security and Privacy in Computing and Communications/13th IEEE International Conference on Big Data Science and Engineering. ed. / Liqun Chen; Ryan Ko; Liming Zhu. Piscataway NJ USA : IEEE, Institute of Electrical and Electronics Engineers, 2019. p. 562-569 8887372.

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

TY - GEN

T1 - A logic for secure stratified systems and its application to containerized systems

AU - Lauer, Hagen

AU - Sakzad, Amin

AU - Rudolph, Carsten

AU - Nepal, Surya

PY - 2019

Y1 - 2019

N2 - We present the design and verification of a secure integrity measurement system for containerized systems. Containerization of applications allows fine-graded deployment and management of services and dependencies but also needs fine-graded security mechanisms. In this paper we provide formal abstractions for containerized systems by introducing LS^3, a formal model and logic with sub-domain constructs to represent stratified systems and their interactions. Using our formal model, we prove that the widely used Trusted Computing Group (TCG) based Integrity Measurement Architecture (IMA) securely extends trust measurements from boot to applications. However, IMA is not designed to make domain specific trust measurements and is consequently incapable of creating domain specific integrity reports. Current research aims to improve either trust measurement performance or comprehensiveness but does not improve the measurement function and its semantics to allow remote verification of measurements per domain. We present an enhanced trust measurement architecture design, which produces domain specific integrity measurements suitable for fine-graded remote attestation. Providing domain specific integrity reports eases system and sub-system verification and yields desirable properties such as measurement log stability and constrained disclosure for multi-domain systems. We verify and prove the correctness of our trust measurement architecture using our formal model.

AB - We present the design and verification of a secure integrity measurement system for containerized systems. Containerization of applications allows fine-graded deployment and management of services and dependencies but also needs fine-graded security mechanisms. In this paper we provide formal abstractions for containerized systems by introducing LS^3, a formal model and logic with sub-domain constructs to represent stratified systems and their interactions. Using our formal model, we prove that the widely used Trusted Computing Group (TCG) based Integrity Measurement Architecture (IMA) securely extends trust measurements from boot to applications. However, IMA is not designed to make domain specific trust measurements and is consequently incapable of creating domain specific integrity reports. Current research aims to improve either trust measurement performance or comprehensiveness but does not improve the measurement function and its semantics to allow remote verification of measurements per domain. We present an enhanced trust measurement architecture design, which produces domain specific integrity measurements suitable for fine-graded remote attestation. Providing domain specific integrity reports eases system and sub-system verification and yields desirable properties such as measurement log stability and constrained disclosure for multi-domain systems. We verify and prove the correctness of our trust measurement architecture using our formal model.

KW - Formal Verification

KW - Trusted Computing

KW - Virtualization

UR - http://www.scopus.com/inward/record.url?scp=85075184698&partnerID=8YFLogxK

U2 - 10.1109/TrustCom/BigDataSE.2019.00081

DO - 10.1109/TrustCom/BigDataSE.2019.00081

M3 - Conference Paper

SN - 9781728127781

SP - 562

EP - 569

BT - Proceedings - 2019 18th IEEE International Conference on Trust, Security and Privacy in Computing and Communications/13th IEEE International Conference on Big Data Science and Engineering

A2 - Chen, Liqun

A2 - Ko, Ryan

A2 - Zhu, Liming

PB - IEEE, Institute of Electrical and Electronics Engineers

CY - Piscataway NJ USA

ER -

Lauer H, Sakzad A, Rudolph C, Nepal S. A logic for secure stratified systems and its application to containerized systems. In Chen L, Ko R, Zhu L, editors, Proceedings - 2019 18th IEEE International Conference on Trust, Security and Privacy in Computing and Communications/13th IEEE International Conference on Big Data Science and Engineering. Piscataway NJ USA: IEEE, Institute of Electrical and Electronics Engineers. 2019. p. 562-569. 8887372 https://doi.org/10.1109/TrustCom/BigDataSE.2019.00081