kth.sePublications
Change search
Link to record
Permanent link

Direct link
Publications (10 of 48) Show all publications
Dong, N., Guanciale, R., Dam, M. & Lööw, A. (2023). Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor. In: Alexander Nadel; Kristin Yvonne Rozier (Ed.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023: . Paper presented at Formal Methods in Computer-Aided Design (FMCAD) 2023, 24-27 Oct. 2023. TU Wien Academic Press
Open this publication in new window or tab >>Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor
2023 (English)In: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 / [ed] Alexander Nadel; Kristin Yvonne Rozier, TU Wien Academic Press , 2023Conference paper, Published paper (Refereed)
Abstract [en]

We present an in-order pipelined processor and its verification in the HOL4 interactive theorem prover. The processor implements the RISC ISA Silver and features a general 5-stage pipeline. The correctness of the processor is proved by exhibiting a refinement relation between the traces of the pipelined circuit and the Silver ISA. The processor is constructed by using a HOL4 Verilog library for formally verified hardware, and its correctness is guaranteed down to the Verilog implementation. Additionally, we analyze the information flow properties of the processor by utilizing the refinement relation. The notion of conditional noninterference formulates that a processor should not leak more information via its timing channel than what is expected by a leakage model expressed at the ISA level. We establish the conditional noninterference for our processor and demonstrate the adaptability of the information flow methodology to accommodate various processor designs, attacker models, and environments. Our approach to verify processor implementations and enable information flow analysis at the circuit level is suitable for ISAs beyond Silver.

Place, publisher, year, edition, pages
TU Wien Academic Press, 2023
Keywords
Formal Verification, Information Flow, Pipelined Processor, Interactive Theorem Prover
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-338911 (URN)10.34727/2023/isbn.978-3-85448-060-0_33 (DOI)2-s2.0-85180375645 (Scopus ID)
Conference
Formal Methods in Computer-Aided Design (FMCAD) 2023, 24-27 Oct. 2023
Funder
Swedish Foundation for Strategic Research
Note

QC 20231121

Available from: 2023-11-21 Created: 2023-11-21 Last updated: 2024-01-04Bibliographically approved
Larsen, J. K., Guanciale, R., Haller, P. & Scalas, A. (2023). P4R-Type: A Verified API for P4 Control Plane Programs. Proceedings of the ACM on Programming Languages, 7(OOPSLA2), Article ID 290.
Open this publication in new window or tab >>P4R-Type: A Verified API for P4 Control Plane Programs
2023 (English)In: Proceedings of the ACM on Programming Languages, E-ISSN 2475-1421, Vol. 7, no OOPSLA2, article id 290Article in journal (Refereed) Published
Abstract [en]

Software-Defined Networking (SDN) significantly simplifies programming, reconfiguring, and optimizing network devices, such as switches and routers. The de facto standard for programming SDN devices is the P4 language. However, the flexibility and power of P4, and SDN more generally, gives rise to important risks. As a number of incidents at major cloud providers have shown, errors in SDN programs can compromise the availability of networks, leaving them in a non-functional state. The focus of this paper are errors in control-plane programs that interact with P4-enabled network devices via the standardized P4Runtime API. For clients of the P4Runtime API it is easy to make mistakes that may lead to catastrophic failures, despite the use of Google's Protocol Buffers as an interface definition language. This paper proposes P4R-Type, a novel verified P4Runtime API for Scala that performs static checks for P4 control plane operations, ruling out mismatches between P4 tables, allowed actions, and action parameters. As a formal foundation of P4R-Type, we present the FP4R calculus and its typing system, which ensure that well-typed programs never get stuck by issuing invalid P4Runtime operations. We evaluate the safety and flexibility of P4R-Type with 3 case studies. To the best of our knowledge, this is the first work that formalises P4Runtime control plane applications, and a typing discipline ensuring the correctness of P4Runtime operations.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2023
Keywords
P4, P4Runtime, Semantics, Software-defined networking, Type systems
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-339489 (URN)10.1145/3622866 (DOI)001087279100070 ()2-s2.0-85175024779 (Scopus ID)
Note

QC 20231113

Available from: 2023-11-13 Created: 2023-11-13 Last updated: 2024-02-29Bibliographically approved
Bocci, A., Forti, S., Guanciale, R., Ferrari, G.-L. & Brogi, A. (2023). Secure Partitioning of Cloud Applications, with Cost Look-Ahead. Future Internet, 15(7), Article ID 224.
Open this publication in new window or tab >>Secure Partitioning of Cloud Applications, with Cost Look-Ahead
Show others...
2023 (English)In: Future Internet, E-ISSN 1999-5903, Vol. 15, no 7, article id 224Article in journal (Refereed) Published
Abstract [en]

The security of Cloud applications is a major concern for application developers and operators. Protecting users' data confidentiality requires methods to avoid leakage from vulnerable software and unreliable Cloud providers. Recently, trusted execution environments (TEEs) emerged in Cloud settings to isolate applications from the privileged access of Cloud providers. Such hardware-based technologies exploit separation kernels, which aim at safely isolating the software components of applications. In this article, we propose a methodology to determine safe partitionings of Cloud applications to be deployed on TEEs. Through a probabilistic cost model, we enable application operators to select the best trade-off partitioning in terms of future re-partitioning costs and the number of domains. To the best of our knowledge, no previous proposal exists addressing such a problem. We exploit information-flow security techniques to protect the data confidentiality of applications by relying on declarative methods to model applications and their data flow. The proposed solution is assessed by executing a proof-of-concept implementation that shows the relationship among the future partitioning costs, number of domains and execution times.

Place, publisher, year, edition, pages
MDPI AG, 2023
Keywords
data confidentiality, trusted execution environments, separation kernels, information-flow security, deployment costs, declarative programming
National Category
Computer Systems
Identifiers
urn:nbn:se:kth:diva-334315 (URN)10.3390/fi15070224 (DOI)001038674500001 ()2-s2.0-85166392852 (Scopus ID)
Note

QC 20230818

Available from: 2023-08-18 Created: 2023-08-18 Last updated: 2023-08-18Bibliographically approved
Guanciale, R., Baumann, C., Buiras, P., Dam, M. & Nemati, H. (2022). A Case Study in Information Flow Refinement for Low Level Systems. In: The Logic of Software. A Tasting Menu of Formal Methods: (pp. 54-79). Springer Nature
Open this publication in new window or tab >>A Case Study in Information Flow Refinement for Low Level Systems
Show others...
2022 (English)In: The Logic of Software. A Tasting Menu of Formal Methods, Springer Nature , 2022, p. 54-79Chapter in book (Other academic)
Abstract [en]

In this work we employ information-flow-aware refinement to study security properties of a separation kernel. We focus on refinements that support changes in data representation and semantics, including the addition of state variables that may induce new observational power or side channels. We leverage an epistemic approach to ignorance-preserving refinement where an abstract model is used as a specification of a system’s permitted information flows that may include the declassification of secret information. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. In particular, we show that a simple key manager may cause information leakage via a refinement that includes cache and timing information. Finally, we show that deploying standard countermeasures against cache-based timing channels regains ignorance preservation.

Place, publisher, year, edition, pages
Springer Nature, 2022
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 13360
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-318002 (URN)10.1007/978-3-031-08166-8_4 (DOI)2-s2.0-85133695692 (Scopus ID)
Note

QC 20220916

Available from: 2022-09-16 Created: 2022-09-16 Last updated: 2022-09-16Bibliographically approved
Wiggberg, M., Gobena, E., Kaulio, M., Glassey, R., Bälter, O., Hussain, D., . . . Haller, P. (2022). Effective Reskilling of Foreign-Born People at Universities-The Software Development Academy. IEEE Access, 10, 24556-24565
Open this publication in new window or tab >>Effective Reskilling of Foreign-Born People at Universities-The Software Development Academy
Show others...
2022 (English)In: IEEE Access, E-ISSN 2169-3536, Vol. 10, p. 24556-24565Article in journal (Refereed) Published
Abstract [en]

Contribution: An intensive three-month educational program can be used for rapid integration of foreign-born people into the IT industry. A novel method for integrating industrial needs with the practical parts of a bachelor's Computer Science program. Background: The program was motivated by (1) the societal need to increase the meaningful integration of immigrants into the workforce, and (2) the demand for IT specialists in the IT labor market. Intended outcomes: An effective intensive software developer program with a high level of industrial integration and a working matching model for employment. Application design: The program consists of three different phases; recruitment of participants, training and job matching. The training is divided into six modules using five different teaching methods. An evaluation model, based on passive and active data, is implemented with fast learning loops for teachers and participants. Findings: The program has been run seven times with 263 unemployed participants of different nationalities. On average 82.6 percent of the participants found employment in the IT industry within 5 months of the course ending. Female participants are in the majority and are more successful in securing employment. The findings suggest that it was possible to rapidly prototype and deliver an advanced reskilling program within a university setting and use it as a positive method to support newcomers find meaningful work that has a direct benefit for the local IT industry, as well as for the wider society.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2022
Keywords
Education, Training, Employment, Recruitment, Companies, Software, Industries, Accelerated learning, career development, computer-aided instruction, computer science education, curricula development, lifelong learning
National Category
Economics
Identifiers
urn:nbn:se:kth:diva-310257 (URN)10.1109/ACCESS.2022.3152194 (DOI)000766542100001 ()2-s2.0-85124834709 (Scopus ID)
Note

QC 20220325

Available from: 2022-03-25 Created: 2022-03-25 Last updated: 2022-06-25Bibliographically approved
Haglund, J. & Guanciale, R. (2022). Formally Verified Isolation of DMA. In: Alberto Griggio / Neha Rungta (Ed.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022: . Paper presented at 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022, Trento, Italy, October 17-21, 2022. Vienna
Open this publication in new window or tab >>Formally Verified Isolation of DMA
2022 (English)In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 / [ed] Alberto Griggio / Neha Rungta, Vienna, 2022Conference paper, Published paper (Refereed)
Abstract [en]

Every computer having a network, USB or disk controller has a Direct Memory Access Controller (DMAC) which is configured by a driver to transfer data between the device and main memory. The DMAC, if wrongly configured, can therefore potentially leak sensitive data and overwrite critical memory to overtake the system. Since DMAC drivers tend to be buggy (due to their complexity), these attacks are a serious threat.

This paper presents a general formal framework for modeling DMACs and verifying under which conditions they are isolated. These conditions can be used as a specification for guaranteeing that a driver configures the DMAC correctly. The framework provides general isolation theorems that are common to all DMACs, leaving to the user only the task of verifying proof obligations that are DMAC specific. This provides a reusable verification infrastructure that reduces the verification effort of DMACs. Models and proofs have been developed in the HOL4 interactive theorem prover. To demonstrate the usefulness of the framework, we instantiate it with a DMAC of a USB.

Place, publisher, year, edition, pages
Vienna: , 2022
Series
Formal Methods in Computer-Aided Design
Keywords
Formal verification, interactive theorem proving, DMA, I/O security, memory isolation
National Category
Computer Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-327292 (URN)10.34727/2022/isbn.978-3-85448-053-2_18 (DOI)001062691400018 ()2-s2.0-85148065913 (Scopus ID)
Conference
22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022, Trento, Italy, October 17-21, 2022
Note

Part of proceedings ISBN 978-3-85448-053-2

QC 20230526

Available from: 2023-05-23 Created: 2023-05-23 Last updated: 2023-10-16Bibliographically approved
Palmskog, K., Yao, X., Dong, N., Guanciale, R. & Dam, M. (2022). Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution. In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022: . Paper presented at 2022 Formal Methods in Computer-Aided Design (FMCAD), 17-21 October 2022, Trento, Italy (pp. 129-138). Institute of Electrical and Electronics Engineers (IEEE)
Open this publication in new window or tab >>Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution
Show others...
2022 (English)In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022, Institute of Electrical and Electronics Engineers (IEEE) , 2022, p. 129-138Conference paper, Published paper (Refereed)
Abstract [en]

Program analyses based on Instruction Set Architecture (ISA) abstractions can be circumvented using microarchitectural vulnerabilities, permitting unwanted program information flows even when proven ISA-level properties ostensibly rule them out. However, the low abstraction levels found below ISAs, e.g., in microarchitectures defined in hardware description languages, may obscure information flow and hinder analysis tool development. We present a machine-checked formalization in the HOL4 theorem prover of a language, MIL, that abstractly describes microarchitectural in-order and out-of-order program execution and enables reasoning about low-level program information flows. In particular, MIL programs can exhibit information flow side channels when executed out-of-order, as compared to a reference in-order execution. We prove memory consistency between MIL's out-of-order and in-order dynamic semantics in HOL4, and define a notion of conditional noninterference for MIL programs which rules out trace-driven cache side channels. We then demonstrate how to establish conditional noninterference for programs via a novel semi-automated bisimulation based verification strategy inside HOL4 that we apply to several examples. Based on our results, we believe MIL is suitable as a translation target for ISA code to enable information flow analyses.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2022
Series
Formal Methods in Computer-Aided Design
Keywords
HOL4, information flow, interactive theorem proving, microarchitectures, out-of-order execution
National Category
Computer Systems
Identifiers
urn:nbn:se:kth:diva-330691 (URN)10.34727/2022/isbn.978-3-85448-053-2_19 (DOI)001062691400019 ()2-s2.0-85148099314 (Scopus ID)
Conference
2022 Formal Methods in Computer-Aided Design (FMCAD), 17-21 October 2022, Trento, Italy
Note

Part of ISBN 9783854480532

QC 20230630

Available from: 2023-06-30 Created: 2023-06-30 Last updated: 2023-12-21Bibliographically approved
Alshnakat, A., Lundberg, D., Guanciale, R., Dam, M. & Palmskog, K. (2022). HOL4P4: Semantics for a Verified Data Plane. In: EuroP4 2022: Proceedings of the 5th International Workshop on P4 in Europe, Part of CoNEXT 2022. Paper presented at 5th International Workshop on P4 in Europe, EuroP4 2022, co-located with ACM CoNEXT 2022, Rome, Italy, Dec 9 2022 (pp. 39-45). Association for Computing Machinery (ACM)
Open this publication in new window or tab >>HOL4P4: Semantics for a Verified Data Plane
Show others...
2022 (English)In: EuroP4 2022: Proceedings of the 5th International Workshop on P4 in Europe, Part of CoNEXT 2022, Association for Computing Machinery (ACM) , 2022, p. 39-45Conference paper, Published paper (Refereed)
Abstract [en]

We introduce a formal semantics of P4 for the HOL4 interactive theorem prover. We exploit properties of the language, like the absence of call by reference and the copy-in/copy-out mechanism, to define a heapless small-step semantics that is abstract enough to simplify verification, but that covers the main aspects of the language: interaction with the architecture via externs, table match, and parsers. Our formalization is written in the Ott metalanguage, which allows us to export definitions to multiple interactive theorem provers. The exported HOL4 semantics allows us to establish machine-checkable proofs regarding the semantics, properties of P4 programs, and soundness of analysis tools.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2022
Keywords
formal verification, interactive theorem proving, P4, programming language semantics
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-333491 (URN)10.1145/3565475.3569081 (DOI)001062234700007 ()2-s2.0-85145586258 (Scopus ID)
Conference
5th International Workshop on P4 in Europe, EuroP4 2022, co-located with ACM CoNEXT 2022, Rome, Italy, Dec 9 2022
Note

Part of ISBN 9781450399357

QC 20230802

Available from: 2023-08-02 Created: 2023-08-02 Last updated: 2023-10-16Bibliographically approved
Bocci, A., Guanciale, R., Forti, S., Ferrari, G.-L. & Brogi, A. (2022). Secure Partitioning of Composite Cloud Applications. In: Montesi, F Papadopoulos, GA Zimmermann, W (Ed.), Service-Oriented and Cloud Computing: . Paper presented at 9th IFIP WG 6.12 European Conference on Service-Oriented and Cloud Computing (ESOCC), MAR 22-24, 2022, ELECTR NETWORK (pp. 47-64). Springer Nature, 13226
Open this publication in new window or tab >>Secure Partitioning of Composite Cloud Applications
Show others...
2022 (English)In: Service-Oriented and Cloud Computing / [ed] Montesi, F Papadopoulos, GA Zimmermann, W, Springer Nature , 2022, Vol. 13226, p. 47-64Conference paper, Published paper (Refereed)
Abstract [en]

The security of Cloud applications is always a major concern for application developers and operators. Protecting their users' data confidentiality requires methods to avoid leakage from vulnerable software and unreliable cloud providers. Recently, hardware-based technologies emerged in the Cloud setting to isolate applications from the privileged access of cloud providers. One of those technologies is the Separation Kernel which aims at isolating safely the software components of applications. In this article, we propose a declarative methodology supported by a running prototype to determine the partitioning of a Cloud multi-component application in order to allow its placement on a Separation Kernel. We employ information-flow security techniques to determine how to partition the application, and showcase the methodology and prototype over a motivating scenario from an IoT application deployed to a central Cloud.

Place, publisher, year, edition, pages
Springer Nature, 2022
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 13226
Keywords
Data Confidentiality, Separation Kernel, Information-flow Security
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-321265 (URN)10.1007/978-3-031-04718-3_3 (DOI)000876716400003 ()2-s2.0-85128987312 (Scopus ID)
Conference
9th IFIP WG 6.12 European Conference on Service-Oriented and Cloud Computing (ESOCC), MAR 22-24, 2022, ELECTR NETWORK
Note

QC 20221111

Part of proceedings: ISBN 978-3-031-04718-3; 978-3-031-04717-6

Available from: 2022-11-11 Created: 2022-11-11 Last updated: 2022-11-11Bibliographically approved
Guanciale, R., Paladi, N. & Vahidi, A. (2022). SoK: Confidential Quartet - Comparison of Platforms for Virtualization-Based Confidential Computing. In: 2022 IEEE international symposium on secure and private execution environment design (SEED 2022): . Paper presented at IEEE International Symposium on Secure and Private Execution Environment Design (SEED), SEP 26-27, 2022, ELECTR NETWORK (pp. 109-120). Institute of Electrical and Electronics Engineers (IEEE)
Open this publication in new window or tab >>SoK: Confidential Quartet - Comparison of Platforms for Virtualization-Based Confidential Computing
2022 (English)In: 2022 IEEE international symposium on secure and private execution environment design (SEED 2022), Institute of Electrical and Electronics Engineers (IEEE) , 2022, p. 109-120Conference paper, Published paper (Refereed)
Abstract [en]

Confidential computing allows processing sensitive workloads in securely isolated spaces. Following earlier adoption of process-based approaches to isolation, vendors are now enabling hardware and firmware support for virtualization-based confidential computing on several server platforms. Due to variations in the technology stack, threat model, implementation and functionality, the available solutions offer somewhat different capabilities, trade-offs and security guarantees. In this paper we review, compare and contextualize four virtualization-based confidential computing technologies for enterprise server platforms - AMD SEV, ARM CCA, IBM PEF and Intel TDX.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2022
Keywords
Confidential Computing
National Category
Computer Sciences Computer Systems
Identifiers
urn:nbn:se:kth:diva-322795 (URN)10.1109/SEED55351.2022.00017 (DOI)000889465400010 ()2-s2.0-85143079315 (Scopus ID)
Conference
IEEE International Symposium on Secure and Private Execution Environment Design (SEED), SEP 26-27, 2022, ELECTR NETWORK
Note

Part of proceedings ISBN 978-1-6654-8526-5QC 20230131

Available from: 2023-01-31 Created: 2023-01-31 Last updated: 2023-01-31Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-8069-6495

Search in DiVA

Show all publications