| 1. |
- Alshnakat, Anoud, et al.
(författare)
-
HOL4P4 : Semantics for a Verified Data Plane
- 2022
-
Ingår i: EuroP4 2022. - New York, NY, USA : Association for Computing Machinery (ACM). ; , s. 39-45
-
Konferensbidrag (refereegranskat)abstract
- 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. |
- Alshnakat, Anoud, et al.
(författare)
-
HOL4P4: Mechanized Small-Step Semantics for P4
- 2024
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 8:OOPSLA1
-
Tidskriftsartikel (refereegranskat)abstract
- We present the first semantics of the network data plane programming language P4 able to adequately capture all key features of P416, the most recent version of P4, including external functions (externs) and concurrency. These features are intimately related since, in P4, extern invocations are the only points at which one execution thread can affect another. Reflecting P4's lack of a general-purpose memory and the presence of multithreading the semantics is given in small-step style and eschews the use of a heap. In addition to the P4 language itself, we provide an architectural level semantics, which allows the composition of P4-programmed blocks, models end-to-end packet processing, and can take into account features such as arbitration and packet recirculation. A corresponding type system is provided with attendant progress, preservation, and type-soundness theorems. Semantics, type system, and meta-theory are formalized in the HOL4 theorem prover. From this formalization, we derive a HOL4 executable semantics that supports verified execution of programs with partially symbolic packets able to validate simple end-to-end program properties.
|
|
| 3. |
- Balliu, Musard, et al.
(författare)
-
Automating Information Flow Analysis of Low Level Code
- 2014
-
Ingår i: Proceedings of CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA. - New York, NY, USA : Association for Computing Machinery (ACM). - 9781450329576
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 4. |
- Balliu, Musard, et al.
(författare)
-
InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis.
-
Annan publikation (övrigt vetenskapligt/konstnärligt)abstract
- 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).
|
|
| 5. |
- Baumann, Christoph, et al.
(författare)
-
On Compositional Information Flow Aware Refinement
- 2021
-
Ingår i: 2021 IEEE 34Th Computer Security Foundations Symposium (CSF 2021). - : Institute of Electrical and Electronics Engineers (IEEE). ; , s. 17-32
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 6. |
- Bocci, Alessandro, et al.
(författare)
-
Secure Partitioning of Cloud Applications, with Cost Look-Ahead
- 2023
-
Ingår i: Future Internet. - : MDPI AG. - 1999-5903. ; 15:7
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 7. |
- Bocci, Alessandro, et al.
(författare)
-
Secure Partitioning of Composite Cloud Applications
- 2022
-
Ingår i: Service-Oriented and Cloud Computing. - Cham : Springer Nature. ; , s. 47-64
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 8. |
- Buiras, Pablo, et al.
(författare)
-
Validation of side-channel models via observation refinement
- 2021
-
Ingår i: Proceedings of the Annual International Symposium on Microarchitecture, MICRO. - New York, NY, USA : Association for Computing Machinery (ACM). ; , s. 578-591
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 9. |
- Chfouka, Hind, et al.
(författare)
-
Trustworthy prevention of code injection in Linux on embedded devices
- 2015
-
Ingår i: 20th European Symposium on Research in Computer Security, ESORICS 2015. - Cham : Springer. - 9783319241739 ; , s. 90-107
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 10. |
- Coto, Alex, et al.
(författare)
-
An abstract framework for choreographic testing
- 2020
-
Ingår i: Electronic Proceedings in Theoretical Computer Science, EPTCS<em></em>. ; , s. 43-60
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- 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.
|
|
