Endre søk
Begrens søket
1 - 50 of 50
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Treff pr side
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
Merk
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1.
    Alshnakat, Anoud
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Lundberg, Didrik
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS. Saab AB, Järfälla, Sweden.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Palmskog, Karl
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    HOL4P4: Semantics for a Verified Data Plane2022Inngår i: EuroP4 2022: Proceedings of the 5th International Workshop on P4 in Europe, Part of CoNEXT 2022, Association for Computing Machinery (ACM) , 2022, s. 39-45Konferansepaper (Fagfellevurdert)
    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.

  • 2.
    Balliu, Musard
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Automating Information Flow Analysis of Low Level Code2014Inngår i: Proceedings of CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA, Association for Computing Machinery (ACM), 2014Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Low level code is challenging: It lacks structure, it uses jumps and symbolic addresses, the control ow is often highly optimized, and registers and memory locations may be reused in ways that make typing extremely challenging. Information ow properties create additional complications: They are hyperproperties relating multiple executions, and the possibility of interrupts and concurrency, and use of devices and features like memory-mapped I/O requires a departure from the usual initial-state nal-state account of noninterference. In this work we propose a novel approach to relational verication for machine code. Verication goals are expressed as equivalence of traces decorated with observation points. Relational verication conditions are propagated between observation points using symbolic execution, and discharged using rst-order reasoning. We have implemented an automated tool that integrates with SMT solvers to automate the verication task. The tool transforms ARMv7 binaries into an intermediate, architecture-independent format using the BAP toolset by means of a veried translator. We demonstrate the capabilities of the tool on a separation kernel system call handler, which mixes hand-written assembly with gcc-optimized output, a UART device driver and a crypto service modular exponentiation routine.

    Fulltekst (pdf)
    ccs14_bdg
  • 3.
    Balliu, Musard
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis.Manuskript (preprint) (Annet vitenskapelig)
    Abstract [en]

    The recent Spectre attacks has demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation to extract arbitrary information about the memory contents of a process. A comprehensive formal microarchitectural model capable of representing the forms of out-of-order and speculative behavior that can meaningfully be implemented in a high performance pipelined architecture has not yet emerged. Such a model would be very useful, as it would allow the existence and non-existence of vulnerabilities, and soundness of countermeasures to be formally established. In this paper we present such a model targeting single core processors. The model is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that underpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities, as well as to formally analyze the effectiveness of proposed countermeasures. Specifically, we discover three new (potential) vulnerabilities, including a new variant of Spectre v4, a vulnerability on speculative fetching, and a vulnerability on out-of-order execution, and analyze the effectiveness of three existing countermeasures: constant time, Retpoline, and ARM's Speculative Store Bypass Safe (SSBS).

    Fulltekst (pdf)
    fulltext
  • 4.
    Baumann, Christoph
    et al.
    Ericsson Research Security, Kista, Sweden.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Nemati, Hamed
    Helmholtz Center for Information Security (CISPA), Saarbrücken, Germany.
    On Compositional Information Flow Aware Refinement2021Inngår i: 2021 IEEE 34Th Computer Security Foundations Symposium (CSF 2021), Institute of Electrical and Electronics Engineers (IEEE) , 2021, s. 17-32Konferansepaper (Fagfellevurdert)
    Abstract [en]

    The concepts of information flow security and refinement are known to have had a troubled relationship ever since the seminal work of McLean. In this work we study 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 propose a new 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. Our study is set in the context of a class of shared variable multi-agent models similar to interpreted systems in epistemic logic. We demonstrate the expressiveness of our framework through a series of small examples and compare our approach to existing, stricter notions of information-flow secure refinement based on bisimulations and noninterference preservation. Interestingly, noninterference preservation is not supported "out of the box" in our setting, because refinement steps may introduce new secrets that are independent of secrets already present at abstract level. To support verification, we first introduce a "cube-shaped" unwinding condition related to conditions recently studied in the context of value-dependent noninterference, kernel verification, and secure compilation. A fundamental problem with ignorance-preserving refinement, caused by the support for general data and observation refinement, is that sequential composability is lost. We propose a solution based on relational pre- and post-conditions and illustrate its use together with unwinding on the oblivious RAM construction of Chung and Pass.

  • 5.
    Bocci, Alessandro
    et al.
    Univ Pisa, Dept Comp Sci, I-56127 Pisa, Italy..
    Forti, Stefano
    Univ Pisa, Dept Comp Sci, I-56127 Pisa, Italy..
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Ferrari, Gian-Luigi
    Univ Pisa, Dept Comp Sci, I-56127 Pisa, Italy..
    Brogi, Antonio
    Univ Pisa, Dept Comp Sci, I-56127 Pisa, Italy..
    Secure Partitioning of Cloud Applications, with Cost Look-Ahead2023Inngår i: Future Internet, E-ISSN 1999-5903, Vol. 15, nr 7, artikkel-id 224Artikkel i tidsskrift (Fagfellevurdert)
    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.

  • 6.
    Bocci, Alessandro
    et al.
    Univ Pisa, Pisa, Italy..
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Forti, Stefano
    Univ Pisa, Pisa, Italy..
    Ferrari, Gian-Luigi
    Univ Pisa, Pisa, Italy..
    Brogi, Antonio
    Univ Pisa, Pisa, Italy..
    Secure Partitioning of Composite Cloud Applications2022Inngår i: Service-Oriented and Cloud Computing / [ed] Montesi, F Papadopoulos, GA Zimmermann, W, Springer Nature , 2022, Vol. 13226, s. 47-64Konferansepaper (Fagfellevurdert)
    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.

  • 7.
    Buiras, Pablo
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Nemati, Hamed
    Stanford University and CISPA Helmholtz Center for Information Security, United States.
    Lindner, Andreas
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Validation of side-channel models via observation refinement2021Inngår i: Proceedings of the Annual International Symposium on Microarchitecture, MICRO, Association for Computing Machinery (ACM) , 2021, s. 578-591Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Observational models enable the analysis of information flow properties against side channels. Relational testing has been used to validate the soundness of these models by measuring the side channel on states that the model considers indistinguishable. However, unguided search can generate test states that are too similar to each other to invalidate the model. To address this we introduce observation refinement, a technique to guide the exploration of the state space to focus on hardware features of interest. We refine observational models to include fine-grained observations that characterize behavior that we want to exclude. States that yield equivalent refined observations are then ruled out, reducing the size of the space. We have extended an existing model validation framework, Scam-V, to support refinement. We have evaluated the usefulness of refinement for search guidance by analyzing cache coloring and speculative leakage in the ARMv8-A architecture. As a surprising result, we have exposed SiSCLoak, a new vulnerability linked to speculative execution in Cortex-A53.

  • 8. Chfouka, H.
    et al.
    Corradini, A.
    Guanciale, Robert
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Classification techniques for conformance and performance checking in process analysis2013Inngår i: CEUR Workshop Proceedings, ISSN 1613-0073, E-ISSN 1613-0073, Vol. 1101, s. 21-30Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Standard process analysis techniques, like conformance checking or performance evaluation, are enabled by the existence of event logs that trace the process executions and by the presence of a model that formally represents the process. Such analysis techniques use only part of the huge amount of data recorded in event logs. In this paper the goal is to exploit this data to extract useful information for conformance checking and performance analysis. We present an approach that using standard classification technique, explores how data inuence process behaviors by affecting its conformance or performance.

  • 9. Chfouka, Hind
    et al.
    Nemati, Hamed
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Ekdahl, P.
    Ericsson AB.
    Trustworthy prevention of code injection in Linux on embedded devices2015Inngår i: 20th European Symposium on Research in Computer Security, ESORICS 2015, Springer, 2015, s. 90-107Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present MProsper, a trustworthy system to prevent code injection in Linux on embedded devices. MProsper is a formally verified run-time monitor, which forces an untrusted Linux to obey the executable space protection policy; a memory area can be either executable or writable, but cannot be both. The executable space protection allows the MProsper’s monitor to intercept every change to the executable code performed by a user application or by the Linux kernel. On top of this infrastructure, we use standard code signing to prevent code injection. MProsper is deployed on top of the Prosper hypervisor and is implemented as an isolated guest. Thus MProsper inherits the security property verified for the hypervisor: (i) Its code and data cannot be tampered by the untrusted Linux guest and (ii) all changes to the memory layout is intercepted, thus enabling MProsper to completely mediate every operation that can violate the desired security property. The verification of the monitor has been performed using the HOL4 theorem prover and by extending the existing formal model of the hypervisor with the formal specification of the high level model of the monitor.

    Fulltekst (pdf)
    fulltext
  • 10. Coto, A.
    et al.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Tuosto, E.
    On Testing Message-Passing Components2020Inngår i: Leveraging Applications of Formal Methods, Verification and Validation, Springer Nature , 2020, Vol. 12476, s. 22-38Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We instantiate and apply a recently proposed abstract framework featuring an algorithm for the automatic generation of tests for component testing of message-passing systems. We demonstrate the application of a top-down mechanism for test generation. More precisely, we reduce the problem of generating tests for components of message-passing applications to the projection of global views of choreographies. The application of the framework to some examples gives us the pretext to make some considerations about our approach.

  • 11.
    Coto, Alex
    et al.
    Gran Sasso Sci Inst IT, Laquila, Italy..
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Tuosto, Emilio
    Gran Sasso Sci Inst IT, Laquila, Italy..
    An abstract framework for choreographic testing2021Inngår i: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 123, artikkel-id 100712Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present a tool-supported approach for the model-driven testing of message-passing applications. Our approach envisages choreographies as a particularly suited model to derive tests in order to tame the problems of correctness of distributed applications.

  • 12.
    Coto, Alex
    et al.
    GSSI.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Tuosto, Emilio
    GSSI.
    An abstract framework for choreographic testing2020Inngår i: Electronic Proceedings in Theoretical Computer Science, EPTCS / [ed] Lange J., Mavridou A., Safina L., Scalas A., 2020, s. 43-60Konferansepaper (Annet vitenskapelig)
    Abstract [en]

    We initiate the development of a model-driven testing framework for message-passing systems. The notion of test for communicating systems cannot simply be borrowed from existing proposals. Therefore, we formalize a notion of suitable distributed tests for a given choreography and devise an algorithm that generates tests as projections of global views. Our algorithm abstracts away from the actual projection operation, for which we only set basic requirements. The algorithm can be instantiated by reusing existing projection operations (designed to generate local implementations of global models) as they satisfy our requirements. Finally, we show the correctness of the approach and validate our methodology via an illustrative example.

  • 13.
    Coto, Alex
    et al.
    Gran Sasso Science InstituteL’AquilaItaly.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Tuosto, Emilio
    Gran Sasso Science InstituteL’AquilaItaly.
    Choreographic development of message-passing applications: a tutorial2020Inngår i: Lecture Notes in Computer Science book series, Springer , 2020, Vol. 12134, s. 20-36Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Choreographic development envisages distributed coordination as determined by interactions that allow peer components to harmoniously realise a given task. Unlike in orchestration-based coordination, there is no special component directing the execution. Recently, choreographic approaches have become popular in industrial contexts where reliability and scalability are crucial factors. This tutorial reviews some recent ideas to harness choreographic development of message-passing software. The key features of the approach are showcased within, a toolchain which allows software architects to identify defects of message-passing applications at early stages of development.

  • 14.
    Dam, Mads
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Khakpour, Narges
    Nemati, Hamed
    Schwarz, Oliver
    Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel2013Konferansepaper (Fagfellevurdert)
    Abstract [en]

    A separation kernel simulates a distributed environment us-ing a single physical machine by executing partitions in iso-lation and appropriately controlling communication amongthem. We present a formal verication of information owsecurity for a simple separation kernel for ARMv7. Previouswork on information ow kernel security leaves communica-tion to be handled by model-external means, and cannot beused to draw conclusions when there is explicit interactionbetween partitions. We propose a dierent approach wherecommunication between partitions is made explicit and theinformation ow is analyzed in the presence of such a chan-nel. Limiting the kernel functionality as much as meaning-fully possible, we accomplish a detailed analysis and veri-cation of the system, proving its correctness at the levelof the ARMv7 assembly. As a sanity check we show howthe security condition is reduced to noninterference in thespecial case where no communication takes place. The ver-ication is done in HOL4 taking the Cambridge model ofARM as basis, transferring verication tasks on the actualassembly code to an adaptation of the BAP binary analysistool developed at CMU.

    Fulltekst (pdf)
    ccs13_dam_prosper_kernel_verification.pdf
  • 15.
    Dam, Mads
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Nemati, Hamed
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Machine Code Verification of a Tiny ARM Hypervisor2013Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Hypervisors are low level execution platforms that provideisolated partitions on shared resources, allowing to design se-cure systems without using dedicated hardware devices. Akey requirement of this kind of solution is the formal verifi-cation of the software trusted computing base, preferably atthe binary level. We accomplish a detailed verification of anARMv7 tiny hypervisor, proving its correctness at the ma-chine code level. We present our verification strategy, whichmixes the usage of the theorem prover HOL4, the computa-tion of weakest preconditions, and the use of SMT solvers tolargely automate the verification process. The automationrelies on an integration of HOL4 with BAP, the Binary Anal-ysis Platform developed at CMU. To enable the adoption ofthe BAP back-ends to compute weakest preconditions andcontrol flow graphs, a HOL4-based tool was implementedthat transforms ARMv7 assembly programs to the BAP In-termediate Language. Since verifying contracts by comput-ing the weakest precondition depends on resolving indirectjumps, we implemented a procedure that integrates SMTsolvers and BAP to discover all the possible assignments tothe indirect jumps under the contract precondition.

    Fulltekst (pdf)
    trusted13_dam_prosper_machine_code_verification.pdf
  • 16.
    Dong, Ning
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Refinement-Based Verification of Device-to-Device Information Flow2021Inngår i: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021, TU Wien Academic Press , 2021Konferansepaper (Fagfellevurdert)
    Abstract [en]

    I/O devices are the critical components that allow a computing system to communicate with the external environment. From the perspective of a device, interactions can be divided into two parts, with the processor (mainly memory operations by the driver) and through the communication medium with external devices. In this paper, we present an abstract model of I/O devices and their drivers to describe the expected results of their execution, where the communication between devices is made explicit and the device-to-device information flow is analyzed. In order to handle general I/O functionalities, both half-duplex (transmission and reception) and full-duplex (sending and receiving simultaneously) data transmissions are considered. We propose a refinement-based approach that concretizes a correct-by-construction abstract model into an actual hardware device and its driver. As an example, we formalize the Serial Peripheral Interface (SPI) with a driver. In the HOL4 interactive theorem prover, we verified the refinement between these models by establishing a weak bisimulation. We show how this result can be used to establish both functional correctness and information flow security for both single devices and when devices are connected in an end-to-end fashion.

    Fulltekst (pdf)
    fulltext
  • 17.
    Dong, Ning
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Lööw, Andreas
    Imperial College London.
    Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor2023Inngår i: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 / [ed] Alexander Nadel; Kristin Yvonne Rozier, TU Wien Academic Press , 2023Konferansepaper (Fagfellevurdert)
    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.

  • 18.
    Dong, Ning
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Lööw, Andreas
    Imperial College London.
    Information Flow Analysis of a Verified In-Order Pipelined ProcessorManuskript (preprint) (Annet vitenskapelig)
    Abstract [en]

    We implement a verified in-order pipelined processor Silver-Pi for the RISC ISA Silver in the HOL4 interactive theorem prover. The correctness of the processor is established by exhibiting a trace relation between the circuit and the Silver ISA. Based on the correctness proof, we prove the conditional noninterference (CNI) of the processor. The CNI formulates that executing programs on the processor does not leak additional information on the timing channel than permitted by a leakage function expressed at the ISA level.

    Fulltekst (pdf)
    fulltext
  • 19. Emilio, Tuosto
    et al.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Semantics of global view of choreographies2017Inngår i: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 95Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We propose two abstract semantics of the global view of choreographies given in terms of partial orders. The first semantics is formalised as pomsets of communication events while the second one is based on hypergraphs of events. These semantics can accommodate different levels of abstractions. We discuss the adequacy of our models by considering their relation with communicating machines, that we use to formalise the local view. Our approach increases expressiveness and allows us to overcome some limitations that affect alternative semantics of global views. This will be illustrated by discussing some interesting examples. Finally, we show that the two semantics are equivalent and have different merits. More precisely, the semantics based on pomsets yields a more elegant presentation, but it is less suitable for implementation. The semantics based on hypergraphs instead is amenable to a straightforward implementation.

  • 20.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    DiRPOMS: Automatic Checker of Distributed Realizability of POMSets2019Inngår i: COORDINATION 2019: Coordination Models and Languages, Springer, 2019Konferansepaper (Fagfellevurdert)
    Abstract [en]

    DiRPOMS permits to verify if the specification of a distributed system can be faithfully realised via distributed agents that communicate using asynchronous message passing. A distinguishing feature of DiRPOMS is the usage of set of pomsets to specify the distributed system. This provides two benefits: syntax obliviousness and efficiency. By defining the semantics of a coordination language in term of pomsets, it is possible to use DiRPOMS for several coordination models. Also, DiRPOMS can analyze pomsets extracted by system logs, when the coordination model is unknown, and therefore can support coordination mining activities. Finally, by using sets of pomsets in place of flat languages, DiRPOMS can reduce exponential blows of analysis that is typical in case of multiple threads due to interleaving. (Demo video available at https://youtu.be/ISYdBNMxEDY. Tool available at https://bitbucket.org/guancio/chosem-tools/).

  • 21.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Protecting Instruction Set Randomization from Code Reuse Attacks2018Inngår i: 23rd Nordic Conference on Secure IT Systems, NordSec 2018, Springer Verlag , 2018, s. 421-436Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Instruction Set Randomization (ISR) prevents code injection by randomizing the instruction encoding used by programs, thus preventing an attacker from preparing a payload that can be injected in a victim. In this paper we show that code-reuse attacks can be used to circumvent existing ISR techniques and we demonstrate these attacks on an ARMv7 CPU that has been extended with ISR support. To counter this treat, we propose a new ISR that does not have the same vulnerabilities as the existing solutions, imposes moderate decryption cost, does not require additional memory per instruction, and affords efficient random access to the encrypted code. These properties enable efficient hardware implementation of our solution. In order to evaluate our proposal, we implement the new ISR in a hardware simulator and we compare its overhead with respect to existing ISR. 

  • 22.
    Guanciale, Roberto
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Balliu, Musard
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis2020Inngår i: CCS '20: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications, Association for Computing Machinery (ACM) , 2020Konferansepaper (Fagfellevurdert)
    Abstract [en]

    The recent Spectre attacks have demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation to extract arbitrary information about the memory contents of a process. A comprehensive formal microarchitectural model capable of representing the forms of out-of-order and speculative behavior that can meaningfully be implemented in a high performance pipelined architecture has not yet emerged. Such a model would be very useful, as it would allow the existence and non-existence of vulnerabilities, and soundness of countermeasures to be formally established. This paper presents such a model targeting single core processors. The model is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that underpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities, as well as to formally analyze the effectiveness of proposed countermeasures. Specifically, we discover three new (potential) vulnerabilities, including a new variant of Spectre v4, a vulnerability on speculative fetching, and a vulnerability on out-of-order execution, and analyze the effectiveness of existing countermeasures including constant time and serializing instructions.  

  • 23.
    Guanciale, Roberto
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Baumann, C.
    Buiras, Pablo
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Nemati, H.
    A Case Study in Information Flow Refinement for Low Level Systems2022Inngår i: The Logic of Software. A Tasting Menu of Formal Methods, Springer Nature , 2022, s. 54-79Kapittel i bok, del av antologi (Annet vitenskapelig)
    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.

  • 24.
    Guanciale, Roberto
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Privacy preserving business process fusion2015Inngår i: International Workshops on Business Process Management Workshops, BPM 2014, Springer, 2015, Vol. 202, s. 96-101Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Virtual enterprises (VEs) are temporary and loosely coupled alliances of businesses that join their skills to catch new business opportunities. However, the dependencies among the activities of a prospective VE cross the boundaries of the VE constituents. It is therefore crucial to allow the VE constituents to discover their local views of the interorganizational workflow, enabling each company to re-shape, optimize and analyze the possible local flows that are consistent with the processes of the other VE constituents. We refer to this problem asVE process fusion. Even if it has been widely investigated, no previous work addresses VE process fusion in the presence of privacy constraints. In this paper we demonstrate how private intersection of regular languages can be used as the main building block to implement the privacy preserving fusion of business processes modeled by means of bounded Petri nets.

  • 25.
    Guanciale, Roberto
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Laud, P.
    Business process engineering and secure multiparty computation2015Inngår i: Cryptology and Information Security Series, ISSN 1871-6431, Vol. 13, s. 129-149Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    In this chapter we use secure multiparty computation (SMC) to enable privacy-preserving engineering of inter-organizational business processes. Business processes often involve structuring the activities of several organizations, for example when several potentially competitive enterprises share their skills to form a temporary alliance. One of the main obstacles to engineering the processes that govern such collaborations is the perceived threat to the participants’ autonomy. In particular, the participants can be reluctant to expose their internal processes or logs, as this knowledge can be analyzed by other participants to reveal sensitive information. We use SMC techniques to handle two problems in this context: process fusion and log auditing. Process fusion enables the constituents of a collaboration to discover their local views of the inter-organizational workflow, enabling each company to re-shape, optimize and analyze their local flows. Log auditing enables a participant that owns a business process to check if the partner’s logs match its business process, thus enabling the two partners to discover failures, errors and inefficiencies.

  • 26.
    Guanciale, Roberto
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Laud, Peeter
    Private intersection of regular languages2014Inngår i: Privacy, Security and Trust (PST), 2014 Twelfth Annual International Conference on / [ed] Ali Miri, Urs Hengartner, Nen-Fu Huang, Audun Jøsang, Joaquín García-Alfaro, IEEE conference proceedings, 2014, s. 112-120Konferansepaper (Fagfellevurdert)
    Abstract [en]

    This paper addresses the problem of computing the intersection of regular languages in a privacy-preserving fashion. Private set intersection has been addressed earlier in the literature, but for finite sets only. We discuss the various possibilities for solving the problem efficiently, and argue for an approach based on minimal deterministic finite automata (DFA) as a suitable, non-leaking representation of regular language intersection. We propose two different algorithms for DFA minimization in a secure multiparty computation setting, illustrating different aspects of programming based on universal composability and the constraints this sets on existing algorithms. The implementation of our algorithms is based on the programming language SECREC, executing on the SHAREMIND platform for secure multiparty computation. As one application domain we consider fusion of virtual enterprise business processes.

    Fulltekst (pdf)
    pst14.pdf
  • 27.
    Guanciale, Roberto
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Nemati, Hamed
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Baumann, Christoph
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures2016Inngår i: Proceedings - 2016 IEEE Symposium on Security and Privacy, SP 2016, Institute of Electrical and Electronics Engineers (IEEE), 2016, s. 38-55Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Caches pose a significant challenge to formal proofs of security for code executing on application processors, as the cache access pattern of security-critical services may leak secret information. This paper reveals a novel attack vector, exposing a low-noise cache storage channel that can be exploited by adapting well-known timing channel analysis techniques. The vector can also be used to attack various types of security-critical software such as hypervisors and application security monitors. The attack vector uses virtual aliases with mismatched memory attributes and self-modifying code to misconfigure the memory system, allowing an attacker to place incoherent copies of the same physical address into the caches and observe which addresses are stored in different levels of cache. We design and implement three different attacks using the new vector on trusted services and report on the discovery of an 128-bit key from an AES encryption service running in TrustZone on Raspberry Pi 2. Moreover, we subvert the integrity properties of an ARMv7 hypervisor that was formally verified against a cache-less model. We evaluate well-known countermeasures against the new attack vector and propose a verification methodology that allows to formally prove the effectiveness of defence mechanisms on the binary code of the trusted software.

    Fulltekst (pdf)
    fulltext
  • 28.
    Guanciale, Roberto
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Nemati, Hamed
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Baumann, Christoph
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Provably secure memory isolation for Linux on ARM2016Inngår i: Journal of Computer Security, ISSN 0926-227X, E-ISSN 1875-8924, Vol. 24, nr 6, s. 793-837Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation and verification of a memory virtualization platform for ARMv7-A processors. The design is based on direct paging, an MMU virtualization mechanism previously introduced by Xen. It is shown that this mechanism can be implemented using a compact design, suitable for formal verification down to a low level of abstraction, without penalizing system performance. The verification is performed using the HOL4 theorem prover and uses a detailed model of the processor. We prove memory isolation along with information flow security for an abstract top-level model of the virtualization mechanism. The abstract model is refined down to a transition system closely resembling a C implementation. Additionally, it is demonstrated how the gap between the low-level abstraction and the binary level-can be filled, using tools that check Hoare contracts. The virtualization mechanism is demonstrated on real hardware via a hypervisor hosting Linux and supporting a tamper-proof run-time monitor that provably prevents code injection in the Linux guest.

    Fulltekst (pdf)
    fulltext
  • 29.
    Guanciale, Roberto
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Paladi, Nicolae
    Lund Univ, Stockholm, Sweden.;CanaryBit Lund, Stockholm, Sweden..
    Vahidi, Arash
    Res Inst Sweden RISE, Lund, Sweden..
    SoK: Confidential Quartet - Comparison of Platforms for Virtualization-Based Confidential Computing2022Inngår i: 2022 IEEE international symposium on secure and private execution environment design (SEED 2022), Institute of Electrical and Electronics Engineers (IEEE) , 2022, s. 109-120Konferansepaper (Fagfellevurdert)
    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.

  • 30.
    Guanciale, Roberto
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Tuosto, E.
    Realisability of pomsets via communicating automata2018Inngår i: Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association , 2018, Vol. 279, s. 37-51Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Pomsets are a model of concurrent computations introduced by Pratt. They can provide a syntax-oblivious description of semantics of coordination models based on asynchronous message-passing, such as Message Sequence Charts (MSCs). In this paper, we study conditions that ensure a specification expressed as a set of pomsets can be faithfully realised via communicating automata. Our main contributions are (i) the definition of a realisability condition accounting for termination soundness, (ii) conditions for global specifications with “multi-threaded” participants, and (iii) the definition of realisability conditions that can be decided directly over pomsets. A positive by-product of our approach is the efficiency gain in the verification of the realisability conditions obtained when restricting to specific classes of choreographies characterisable in term of behavioural types.

  • 31.
    Guanciale, Roberto
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Tuosto, Emilio
    An Abstract Semantics of the Global View of Choreographies2016Inngår i: Proceedings 9th Interaction and Concurrency Experience, Open Publishing Association , 2016Konferansepaper (Fagfellevurdert)
    Fulltekst (pdf)
    fulltext
  • 32.
    Guanciale, Roberto
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Tuosto, Emilio
    GSSI, Laquila, Italy.;Univ Leicester, Leicester, Leics, England..
    PomCho: Atool chain for choreographic design2021Inngår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 202, artikkel-id 102535Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present a tool chain for model-driven development of asynchronous message-passing applications. The key features of the tool allow designers to identify misbehaviour leading to unsound communications, to provide counterexamples, and to suggest possible corrections as well as to project global specifications to local models in order to generate executable implementations.

  • 33.
    Guanciale, Roberto
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Tuosto, Emilio
    Gran Sasso Science Institute (IT) and Department of Informatics, University of Leicester, UK.
    Realisability of pomsets2019Inngår i: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 108, s. 69-89Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Pomsets are a model of concurrent computations introduced by Pratt. We adopt pomsets as a syntax-oblivious specification model of distributed systems where coordination happens via asynchronous message-passing. In this paper, we study conditions that ensure a specification expressed as a set of pomsets can be faithfully realised via communicating automata. Our main contributions are (i) the definition of a realisability condition accounting for termination soundness, (ii) conditions accounting for "multi-threaded" participants, and (iii) an algorithm to check our realisability conditions directly over pomsets, (iv) an analysis of the algorithm and its benchmarking attained with a prototype implementation.

    In this paper, we study conditions that ensure a specification expressed as a set of pomsets can be faithfully realised via communicating automata. Our main contributions are (i) the definition of a realisability condition accounting for termination soundness, (ii) conditions accounting for ‘‘multi-threaded’’ participants, and (iii) an algorithm to check our realisability conditions directly over pomsets, (iv) an analysis of the algorithm and its benchmarking attained with a prototype implementation.

  • 34.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Laud, P.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Privacy preserving business process matching2015Inngår i: 2015 13th Annual Conference on Privacy, Security and Trust, IEEE , 2015, s. 36-43Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Business process matching is the activity of checking whether a given business process can interoperate with another one in a correct manner. In case the check fails, it is desirable to obtain information about how the first process can be corrected with as few modifications as possible to achieve interoperability. In case the two business processes belong to two separate enterprises that want to build a virtual enterprise, business process matching based on revealing the business processes poses a clear threat to privacy, as it may expose sensitive information about the inner operation of the enterprises. In this paper we propose a solution to this problem for business processes described by means of service automata. We propose a measure for similarity between service automata and use this measure to devise an algorithm that constructs the most similar automaton to the first one that can interoperate with the second one. To achieve privacy, we implement this algorithm in the programming language SecreC, executing on the Sharemind platform for secure multiparty computation. As a result, only the correction information is leaked to the first enterprise and no more.

  • 35.
    Haglund, Jonas
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Formally Verified Isolation of DMA2022Inngår i: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 / [ed] Alberto Griggio / Neha Rungta, Vienna, 2022Konferansepaper (Fagfellevurdert)
    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.

    Fulltekst (pdf)
    fulltext
  • 36.
    Haglund, Jonas
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    Secure Connected CCTV SystemManuskript (preprint) (Annet vitenskapelig)
  • 37.
    Haglund, Jonas
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Trustworthy isolation of DMA devices2020Inngår i: Journal of Banking and Financial Technology, ISSN 2524-7956Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present a mechanism to trustworthy isolate I/O devices with direct memory access (DMA), which ensures that an isolated I/O device cannot access sensitive memory regions. As a demonstrating platform, we use the network interface controller (NIC) of an embedded system. We develop a run-time monitor that forces NIC reconfigurations, defined by untrusted software, to satisfy a security rule. We formalized the NIC in the HOL4 interactive theorem prover and we verified the design of the isolation mechanism. The verification is based on an invariant that is proved to be preserved by all NIC operations and that ensures that all memory accesses address allowed memory regions only. We demonstrate our approach by extending an existing Virtual Machine Introspection (VMI) with the monitor. The resulting platform prevents code injection in a connected and untrusted Linux.

  • 38.
    Haglund, Jonas
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Trustworthy Isolation of DMA Enabled Devices2019Inngår i: 15th International Conference on Information Systems Security, ICISS 2019, Springer , 2019, s. 35-55Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present a mechanism to trustworthy isolate I/O devices with Direct Memory Access (DMA), which ensures that an isolated I/O device cannot access sensitive memory regions. As a demonstrating platform, we use the Network Interface Controller (NIC) of an embedded system. We develop a run-time monitor that forces NIC reconfigurations, defined by untrusted software, to satisfy a security rule. We formalized the NIC in the HOL4 interactive theorem prover and we verified the design of the isolation mechanism. The verification is based on an invariant that is proved to be preserved by all NIC operations and that ensures that all memory accesses address allowed memory regions only. We demonstrate our approach by extending an existing Virtual Machine Introspection (VMI) with the monitor. The resulting platform prevents code injection in a connected and untrusted Linux (The HOL4 proofs and the source code of the monitor are published at https://github.com/kth-step/NIC-formalization-monitor.).

  • 39.
    Larsen, Jens Kanstrup
    et al.
    DTU Compute, Technical University of Denmark, Richard Petersens Plads, Bygning 321, Kongens Lyngby, 2800, Denmark.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Haller, Philipp
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Scalas, Alceste
    DTU Compute, Technical University of Denmark, Richard Petersens Plads, Bygning 321, Kongens Lyngby, 2800, Denmark.
    P4R-Type: A Verified API for P4 Control Plane Programs2023Inngår i: Proceedings of the ACM on Programming Languages, E-ISSN 2475-1421, Vol. 7, nr OOPSLA2, artikkel-id 290Artikkel i tidsskrift (Fagfellevurdert)
    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.

  • 40.
    Lindner, Andreas
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Proof-Producing Symbolic Execution for Binary Code VerificationManuskript (preprint) (Annet vitenskapelig)
  • 41.
    Lindner, Andreas
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Metere, R.
    TrABin: Trustworthy analyses of binaries2019Inngår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 174, s. 72-89Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a common design: the adoption of hardware-independent intermediate representations, a mechanism to translate architecture dependent code to this representation, and a set of architecture independent analyses that process the intermediate representation. The usage of these platforms to verify software introduces the need for trusting both the correctness of the translation from binary code to intermediate language (called transpilation) and the correctness of the analyses. Achieving a high degree of trust is challenging since the transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encodings (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). Similarly, analyses can use complex transformations (e.g. loop unrolling) and simplifications (e.g. partial evaluation) of the artifacts, whose bugs can jeopardize correctness of the results. We overcome these problems by developing a binary analysis platform on top of the interactive theorem prover HOL4. First, we formally model a binary intermediate language and we prove correctness of several supporting tools (i.e. a type checker). Then, we implement two proof-producing transpilers, which respectively translate ARMv8 and CortexM0 programs to the intermediate language and generate a certificate. This certificate is a HOL4 proofdemonstrating correctness of the translation. As demonstrating analysis, we implement a proof-producing weakest precondition generator, which can be used to verify that a given loop-free program fragment satisfies a contract. Finally, we use an AES encryption implementation to benchmark our platform.

  • 42.
    Lundberg, Didrik
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS. Saab AB.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Lindner, Andreas
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Hoare-Style Logic for Unstructured Programs2020Inngår i: Software Engineering and Formal Methods / [ed] Frank de Boer, Antonio Cerone, Cham: Springer Nature , 2020, s. 193-213Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found. We introduce the novel Hoare-style program logic , which interprets postconditions relative to program points when these are first encountered. The logic can support both partial and total correctness, derive contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of  have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, making it applicable to the ARMv6 and ARMv8 instruction sets.

    Fulltekst (pdf)
    fulltext
  • 43. Metere, R.
    et al.
    Lindner, Andreas
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Sound transpilation from binary to machine-independent code2017Inngår i: 20th Brazilian Symposium on Formal Methods, SBMF 2017, Springer, 2017, Vol. 10623, s. 197-214Konferansepaper (Fagfellevurdert)
    Abstract [en]

    In order to handle the complexity and heterogeneity of modern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent intermediate representations. The usage of these platforms to verify systems down to binary-level is appealing due to the high degree of automation they provide. However, it introduces the need for trusting the correctness of the translation from binary code to intermediate language. Achieving a high degree of trust is challenging since this transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encoding (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). We overcome these problems by formally modeling one of such intermediate languages in the interactive theorem prover HOL4 and by implementing a proof-producing transpiler. This tool translates ARMv8 programs to the intermediate language and generates a HOL4 proof that demonstrates the correctness of the translation in the form of a simulation theorem. We also show how the transpiler theorems can be used to transfer properties verified on the intermediate language to the binary code.

  • 44. Nemati, H.
    et al.
    Baumann, Christoph
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Formal verification of integrity-Preserving countermeasures against cache storage side-channels2018Inngår i: 7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Springer, 2018, Vol. 10804, s. 109-133Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Formal verification of systems-level software such as hypervisors and operating systems can enhance system trustworthiness. However, without taking low level features like caches into account the verification may become unsound. While this is a well-known fact w.r.t. timing leaks, few works have addressed latent cache storage side-channels, whose effects are not limited to information leakage. We present a verification methodology to analyse soundness of countermeasures used to neutralise these channels. We apply the proposed methodology to existing countermeasures, showing that they allow to restore integrity of the system. We decompose the proof effort into verification conditions that allow for an easy adaption of our strategy to various software and hardware platforms. As case study, we extend the verification of an existing hypervisor whose integrity can be tampered using cache storage channels. We used the HOL4 theorem prover to validate our security analysis, applying the verification methodology to a generic hardware model. 

  • 45. Nemati, Hamed
    et al.
    Buiras, Pablo
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Lindner, Andreas
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Jacobs, Swen
    Helmholtz Center for Information Security (CISPA)SaarbrückenGermany.
    Validation of Abstract Side-Channel Models for Computer Architectures2020Inngår i: Lecture Notes in Computer Science book series, Springer , 2020, Vol. 1224, s. 225-248Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs which invalidate the models due to hidden microarchitectural behavior.

  • 46.
    Nemati, Hamed
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Do, Viktor
    Vahidi, Arash
    Trustworthy Memory Isolation of Linux on Embedded Devices2015Inngår i: Trust and Trustworthy Computing, TRUST 2015, Springer Berlin/Heidelberg, 2015, s. 125-142Konferansepaper (Fagfellevurdert)
    Abstract [en]

    The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself, for instance by run-time monitoring. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation and verification of a virtualization platform for the ARMv7-A processor family. Our design is based on direct paging, an MMU virtualization mechanism previously introduced by Xen for the x86 architecture, and used later with minor variants by the Secure Virtual Architecture, SVA. We show that the direct paging mechanism can be implemented using a compact design, suitable for formal verification down to a low level of abstraction, without penalizing system performance. The verification is performed using the HOL4 theorem prover and uses a detailed model of the ARMv7-A ISA, including the MMU. We prove memory isolation of the hosted components along with information flow security for an abstract top level model of the virtualization mechanism. The abstract model is refined down to a HOL4 transition system closely resembling a C implementation. The virtualization mechanism is demonstrated on real hardware via a hypervisor capable of hosting Linux as an untrusted guest.

    Fulltekst (pdf)
    fulltext
  • 47.
    Nemati, Hamed
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Baumann, Christoph
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Formal Analysis of Countermeasures against Cache Storage Side Channels2017Manuskript (preprint) (Annet vitenskapelig)
  • 48.
    Nemati, Hamed
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Trustworthy virtualization of the ARMv7 memory subsystem2015Inngår i: 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015, Springer Berlin/Heidelberg, 2015, s. 578-589Konferansepaper (Fagfellevurdert)
    Abstract [en]

    In order to host a general purpose operating system, hypervisors need to virtualize the CPU memory subsystem. This entails dynamically changing MMU resources, in particular the page tables, to allow a hosted OS to reconfigure its own memory. In this paper we present the verification of the isolation properties of a hypervisor design that uses direct paging. This virtualization approach allows to host commodity Oss without requiring either shadow data structures or specialized hardware support. Our verification targets a system consisting of a commodity CPU for embedded devices (ARMv7), a hypervisor and an untrusted guest running Linux.The verification involves three steps: (i) Formalization of an ARMv7 CPU that includes the MMU, (ii) Formalization of a system behavior that includes the hypervisor and the untrusted guest (iii) Verification of the isolation properties. Formalization and proof are done in the HOL4 theorem prover, thus allowing to re-use the existing HOL4 ARMv7 model developed in Cambridge.

    Fulltekst (pdf)
    fulltext
  • 49.
    Palmskog, Karl
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Yao, Xiaomo
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dong, Ning
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution2022Inngår i: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022, Institute of Electrical and Electronics Engineers (IEEE) , 2022, s. 129-138Konferansepaper (Fagfellevurdert)
    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.

  • 50.
    Wiggberg, Mattias
    et al.
    KTH, Skolan för industriell teknik och management (ITM), Industriell ekonomi och organisation (Inst.).
    Gobena, Elina
    KTH, Skolan för industriell teknik och management (ITM), Industriell ekonomi och organisation (Inst.).
    Kaulio, Matti
    KTH, Skolan för industriell teknik och management (ITM), Industriell ekonomi och organisation (Inst.).
    Glassey, Richard
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Bälter, Olof
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Människocentrerad teknologi, Medieteknik och interaktionsdesign, MID.
    Hussain, Dena
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Beräkningsvetenskap och beräkningsteknik (CST).
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Haller, Philipp
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Effective Reskilling of Foreign-Born People at Universities-The Software Development Academy2022Inngår i: IEEE Access, E-ISSN 2169-3536, Vol. 10, s. 24556-24565Artikkel i tidsskrift (Fagfellevurdert)
    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.

1 - 50 of 50
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf