kth.sePublications
Change search
Refine search result
12 1 - 50 of 67
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1.
    Aktug, Irem
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Provably Correct Runtime Monitoring2009In: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 78, no 5, p. 304-339Article in journal (Refereed)
    Abstract [en]

    Runtime monitoring is an established technique to enforce a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has a copy of the given monitor embedded into it. As the main application of these results we sketch a simple inlining algorithm and show how the two-level annotations can be completed to produce a fully annotated program which is valid in the standard sense of Floyd/Hoare logic. This establishes the mediation property that inlined programs are guaranteed to adhere to the intended policy. Furthermore, validity can be checked efficiently using a weakest precondition based annotation checker, thus preparing the ground for on-device checking of policy adherence in a proof-carrying code setting.

  • 2.
    Aktug, Irem
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Provably correct runtime monitoring (extended abstract)2008In: Fm 2008: Formal Methods, Proceedings / [ed] Cuellar, J; Maibaum, T; Sere, K, 2008, Vol. 5014, p. 262-277Conference paper (Refereed)
    Abstract [en]

    Runtime monitoring is an established technique for enforcing a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has an instance of the given monitor embedded into it, which yields state changes at prescribed points according to the monitor's transition function. As our main application of these results we describe a concrete inliner, and use the annotation scheme to characterize its correctness. For this inliner, correctness of the level II annotations can be decided efficiently by a weakest precondition annotation checker, thus allowing on-device checking of inlining correctness in a proof-carrying code setting.

  • 3.
    Alshnakat, Anoud
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Lundberg, Didrik
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS. Saab AB, Järfälla, Sweden.
    Guanciale, Roberto
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    HOL4P4: Semantics for a Verified Data Plane2022In: EuroP4 2022: Proceedings of the 5th International Workshop on P4 in Europe, Part of CoNEXT 2022, Association for Computing Machinery (ACM) , 2022, p. 39-45Conference paper (Refereed)
    Abstract [en]

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

  • 4.
    Balliu, Musard
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Automating Information Flow Analysis of Low Level Code2014In: Proceedings of CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA, Association for Computing Machinery (ACM), 2014Conference paper (Refereed)
    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.

    Download full text (pdf)
    ccs14_bdg
  • 5.
    Balliu, Musard
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Le Guernic, Gurvan
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    ENCOVER: Symbolic Exploration for Information Flow Security2012In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), IEEE , 2012, p. 30-44Conference paper (Refereed)
    Abstract [en]

    We address the problem of program verification for information flow policies by means of symbolic execution and model checking. Noninterference-like security policies are formalized using epistemic logic. We show how the policies can be accurately verified using a combination of concolic testing and SMT solving. As we demonstrate, many scenarios considered tricky in the literature can be solved precisely using the proposed approach. This is confirmed by experiments performed with ENCOVER, a tool based on Java PathFinder and Z3, which we have developed for epistemic noninterference concolic verification.

  • 6.
    Balliu, Musard
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Le Guernic, Gurvan
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Epistemic Temporal Logic for Information Flow Security2011In: In proc. of th 4e ACM SIGPLAN workshop on Programming Languages and Analysis for Security, 2011Conference paper (Refereed)
    Abstract [en]

    Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing program outputs. This approach is shown to elegantly capture standard notions of noninterference and declassification in the literature as well as information flow properties where sensitive and public data intermingle in delicate ways.

  • 7.
    Baumann, Christoph
    et al.
    Ericsson Research Security, Kista, Sweden.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Nemati, Hamed
    Helmholtz Center for Information Security (CISPA), Saarbrücken, Germany.
    On Compositional Information Flow Aware Refinement2021In: 2021 IEEE 34Th Computer Security Foundations Symposium (CSF 2021), Institute of Electrical and Electronics Engineers (IEEE) , 2021, p. 17-32Conference paper (Refereed)
    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.

  • 8.
    Baumann, Christoph
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Schwarz, Oliver
    RISE SICS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Compositional Verification of Security Properties for Embedded Execution Platforms2017In: PROOFS 2017: 6th International Workshop on Security Proofs for Embedded Systems / [ed] Ulrich Kühne and Jean-Luc Danger and Sylvain Guilley, 2017, Vol. 49, p. 1-16Conference paper (Refereed)
    Abstract [en]

    The security of embedded systems can be dramatically improved through the use of formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system level behaviour, the verifications need precise models of the underlying hardware. Such models are hard to attain, highly complex, and proofs of their security properties may not easily apply to similar but different platforms. This may render verification economically infeasible. To address these issues, we propose a compositional top-down approach to embedded system specification and verification, where the system-on-chip is modeled as a network of distributed automata communicating via paired synchronous message passing. Using abstract specifications for each component allows to delay the development of detailed models for cores, devices, etc., while still being able to verify high level security properties like integrity and confidentiality, and soundly refine the result for different instantiations of the abstract components at a later stage. As a case study, we apply this methodology to the verification of information flow security for an industry scale security-oriented hypervisor on the ARMv8-A platform. The hypervisor statically assigns (multiple) cores to each guest system and implements a rudimentary, but usable, inter guest communication discipline. We have completed a pen-and-paper security proof for the hypervisor down to state transition level and report on a partially completed verification of guest mode security in the HOL4 theorem prover.

    Download full text (pdf)
    fulltext
  • 9. Baumann, Christoph
    et al.
    Schwarz, Oliver
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    On the verification of system-level information flow properties for virtualized execution platforms2019In: Journal of Cryptographic Engineering, ISSN 2190-8508, Vol. 9, no 3, p. 243-261Article in journal (Refereed)
    Abstract [en]

    The security of embedded systems can be dramatically improved through the use of formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system-level behavior, the verifications need precise models of the underlying hardware. Such models are hard to attain, highly complex, and proofs of their security properties may not easily apply to similar but different platforms. This may render verification economically infeasible. To address these issues, we propose a compositional top-down approach to embedded system specification and verification, where the system-on-chip is modeled as a network of distributed automata communicating via paired synchronous message passing. Using abstract specifications for each component allows to delay the development of detailed models for cores, devices, etc., while still being able to verify high-level security properties like integrity and confidentiality, and soundly refine the result for different instantiations of the abstract components at a later stage. As a case study, we apply this methodology to the verification of information flow security for an industry-scale security-oriented hypervisor on the ARMv8-A platform and report on the complete verification of guest mode security properties in the HOL4 theorem prover.

    Download full text (pdf)
    fulltext
  • 10.
    Buchegger, Sonja
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, MadsKTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Secure IT Systems: 20th Nordic Conference, NordSec 2015 Stockholm, Sweden, October 19-21, 2015 Proceedings2015Conference proceedings (editor) (Refereed)
  • 11. Chfouka, Hind
    et al.
    Nemati, Hamed
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Ekdahl, P.
    Ericsson AB.
    Trustworthy prevention of code injection in Linux on embedded devices2015In: 20th European Symposium on Research in Computer Security, ESORICS 2015, Springer, 2015, p. 90-107Conference paper (Refereed)
    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.

    Download full text (pdf)
    fulltext
  • 12. Cohen, M.
    et al.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Lomuscio, A.
    Qu, H.
    A data symmetry reduction technique for temporal-epistemic logic2009In: Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, Springer Berlin/Heidelberg, 2009, p. 69-83Conference paper (Refereed)
    Abstract [en]

    We present a data symmetry reduction approach for model checking temporal-epistemic logic. The technique abstracts the epistemic indistinguishably relation for the knowledge operators, and is shown to preserve temporal-epistemic formulae. We show a method for statically detecting data symmetry in an ISPL program, the input to the temporal-epistemic model checker MCMAS. The experiments we report show an exponential saving in verification time and space while verifying security properties of the NSPK protocol.

  • 13. Cohen, M.
    et al.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Lomuscio, A.
    Russo, F.
    Abstraction in Model Checking Multi-agent Systems2009In: AAMAS '09 Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems, Association for Computing Machinery (ACM), 2009, Vol. 1, p. 710-717Conference paper (Refereed)
    Abstract [en]

    We present an abstraction technique for multi-agent, systems preserving temporal-epistcrnic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting abstract system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic specification holds on the abstract system, the specification also holds on the concrete one. In principle this permits us to model check the abstract system rather than the concrete one, thereby saving time and space in the verification step. We illustrate the abstraction technique with two examples. The first example, a card game, illustrates the potential savings in the cost of model checking a typical MAS scenario. In the second example, the abstraction technique is used to verify a communication protocol with an arbitrarily large data domain.

  • 14. Cohen, M
    et al.
    Lomuscio, A
    Dam, Mads
    Univ London Imperial Coll Sci Technol & Med.
    Qu, H
    A symmetry reduction technique for model checking temporal epistemic logic2009In: 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, p. 721-726Conference paper (Refereed)
    Abstract [en]

    We introduce a symmetry reduction technique for model checking temporal-epistemic properties of multi-agent systems defined in the mainstream interpreted systems framework. The technique, based on counterpart semantics, aims to reduce the set of initial states that need to be considered in a model. We present theoretical results establishing that there are neither false positives nor false negatives in the reduced model. We evaluate the technique by presenting the results of an implementation tested against two well known applications of epistemic logic, the muddy children and the dining cryptographers. The experimental results obtained confirm that the reduction in model checking time can be dramatic, thereby allowing for the verification of hitherto intractable systems.

  • 15.
    Cohen, Mika
    et al.
    KTH, School of Computer Science and Communication (CSC), Numerical Analysis and Computer Science, NADA.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    A complete axiomatization of knowledge and cryptography2007In: 22nd Annual IEEE Symposium On Logic In Computer Science, Proceedings, 2007, p. 77-86Conference paper (Refereed)
    Abstract [en]

    The combination offirst-order epistemic logic with formal cryptography offers a potentially powerful framework for security protocol verification. In this paper cryptography is modelled using private constants and one-way computable operations, as in the Applied Pi-calculus. To give the concept of knowledge a computational justification, we propose a generalized Kripke semantics that uses permutations on the underlying domain of cryptographic messages to reflect agents' limited resources. This interpretation links the logic tightly to static equivalence, another important concept of knowledge that has recently been examined in the security protocol literature, and for which there are strong computational soundness results. We exhibit an axiomatization which is sound and complete relative to the underlying theory of terms, and to an omega-rule for quantifiers. Besides standard axioms and rules, the axiomatization includes novel axioms for the interaction between knowledge and cryptography. As protocol examples we use mixes, a Crowds-style protocol, and electronic payments. Funher more, we provide embedding results for BAN and SVO.

  • 16.
    Cohen, Mika
    et al.
    KTH, School of Information and Communication Technology (ICT), Microelectronics and Information Technology, IMIT.
    Dam, Mads
    KTH, School of Information and Communication Technology (ICT), Microelectronics and Information Technology, IMIT.
    Epistemic logic, Cryptography, Logical Omniscience, BAN Logic2005Conference paper (Refereed)
    Abstract [en]

    BAN logic is an epistemic logic for verifying cryptographic protocols. While BAN has been quite successful from a practical point of view, the semantics of the epistemic modality is unclear. Several Kripke semantics have been proposed, but they do not attempt at anything beyond a soundness result. Completeness is prevented by the so called logical omniscience problem: Agents in BAN can draw only feasibly computable consequences of their knowledge, whereas agents in Kripke semantics are not so constrained. To circumvent this problem, we index the epistemic possibility relation of Kripke semantics with a message renaming, relating how cipher texts at the current state correspond to cipher texts at the epistemically possible state. An agent is said to know a property of a message if corresponding messages at epistemically possible states satisfy that property. We obtain completeness with respect to message passing systems, and decidability, by transferring canonical model and filtration constructions from Kripke semantics.

  • 17.
    Cohen, Mika
    et al.
    KTH, School of Information and Communication Technology (ICT), Microelectronics and Information Technology, IMIT.
    Dam, Mads
    KTH, School of Information and Communication Technology (ICT), Microelectronics and Information Technology, IMIT.
    Logical Omniscience in the Semantics of BAN Logics2005Conference paper (Refereed)
    Abstract [en]

    BAN logic is an epistemic logic for verification of cryptographic protocols. A number of semantics have been proposed for BAN logic, but none of them capture the intended meaning of the epistemic modality in a satisfactory way. This is due to the so-called logical omniscience problem : Agents are ”ideal reasoners” in existing semantics, while agents in BAN logic have only limited cryptographic reasoning powers. Logical omniscience is unavoidable in Kripke semantics, the standard semantical framework in epistemic logic. Our proposal is to generalize the epistemic accessibility relation of Kripke semantics so that it changes not only the current execution point, but also the currently predicated message. When  nstantiated on message passing systems, the semantics validates BAN logic. It makes agents introspective (”self-aware”) of their own knowledge and of their own actions of sending, receiving and extracting.

  • 18.
    Costa, Matteo
    et al.
    KTH, School of Industrial Engineering and Management (ITM), Energy Technology.
    Harrucksteiner, Alexander
    KTH, School of Industrial Engineering and Management (ITM), Energy Technology.
    Malusà, Sandro
    KTH, School of Industrial Engineering and Management (ITM), Energy Technology.
    Oggioni, Niccolò
    KTH, School of Industrial Engineering and Management (ITM), Energy Technology.
    Sebastiani, Alessandro
    KTH, School of Industrial Engineering and Management (ITM), Energy Technology.
    van Dam, Benjamin
    KTH, School of Industrial Engineering and Management (ITM), Energy Technology.
    A future view on the Nakano district2018Report (Other academic)
    Abstract [en]

    This project is about reshaping the environment and energy system of Nakano, a residential district inside the city of Tokyo. A qualitative model has been designed, setting the system boundaries and the main features in it. In a second step, ideas about our vision of Nakano in 2040 were developed. The proposed ideas deal with energy, such as the introduction of renewables, but also economics, such as the drop of battery prices, and social well-being, such as the introduction of green areas in the ward.

    In our vision for a more sustainable Nakano, a bicycle highway would be introduced and along this, PV panels would be installed to provide shading and electricity generation at the same time. By 2040, cars could represent a service rather than a property. Currently, most of them are fossil-fuel powered and our idea is that this would drastically change. Furthermore, a sustainable car sharing system using autonomous electric vehicles (EVs) was designed. Urban planning has been treated, dealing with converting low-rise buildings into larger apartment buildings to increase the green areas across theward and enhance the building quality. Building quality and performance have also been a core part in the project due to the poor indoor thermal comfort that currently dominates buildings in Nakano.

    Economic assumptions for 2040 have been made, especially about price trends for the main technologies introduced in the different scenarios. In order to introduce our ideas in the system and see how they would affect it, we developed four different scenarios, each one generated by different assumptions and energy mixes. These are, Business-as-Usual (BAU), in which current trends are generally followed; Renewable and Nuclear (R&N), where renewables and nuclear are set to be the main actors in the energy supply sector; Zero Nuclear Policy (0-Nuclear), in which nuclear energy has been phased out and, as a consequence, renewables are supposed to meet the entire demand together with the grid; and The Ocean and the Sun (O&S), where nuclear energy is still phased out and ocean energy and large scale solar PV are the new energy sources introduced in the energy mix of the ward.

    The whole project was aimed at fulfilling the goals regarding the KPIs. At the end of the report, the results have been shown compared to the original targets. It was proven that reaching every KPI’s target in every scenario was neither technologically nor economically feasible. Anyhow, still a lot of targets were met, and significant improvements compared to today’s conditions of the ward were achieved. Finally, since time is finite, a lot of future work remains that could be a veryinteresting addition to this study about a sustainable future for Nakano.

    Download full text (pdf)
    Nakano-SustainableTokyo2040
  • 19.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Decidability and proof systems for language-based noninterference relations2006In: SIGPLAN notices, ISSN 0362-1340, E-ISSN 1558-1160, Vol. 41, no 1, p. 67-78Article in journal (Refereed)
    Abstract [en]

    Noninterference is the basic semantical condition used to account for confidentiality and integrity-related properties in programming languages. There appears to be an at least implicit belief in the programming languages community that partial approaches based on type systems or other static analysis techniques are necessary for noninterference analyses to be tractable. In this paper we show that this belief is not necessarily true. We focus on the notion of strong low bisimulation proposed by Sabelfeld and Sands. We show that, relative to a decidable expression theory, strong low bisimulation is decidable for a simple parallel while-language, and we give a sound and relatively complete proof system for deriving noninterference assertions. The completeness proof provides an effective proof search strategy. Moreover, we show that common alternative noninterference relations based on traces or input-output relations are undecidable. The first part of the paper is cast in terms of multi-level security. In the second part of the paper we generalize the setting to accommodate a form of intransitive interference. We discuss the model and show how the decidability and proof system results generalize to this richer setting.

  • 20.
    Dam, Mads
    KTH, School of Information and Communication Technology (ICT), Microelectronics and Information Technology, IMIT.
    Regular SPKI2005In: Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349, Vol. 3364, p. 134-152Article in journal (Refereed)
    Abstract [en]

    SPKI is a certificate-based framework for authorisation in distributed systems. The SPKI framework is extended by an iteration construct, essentially Kleene star, to express constraints on delegation chains. Other possible applications, not explored in the paper, include multidomain network routing path constraints. The main decision problems for the extended language are shown to correspond to regular language membership and containment respectively. To support an efficient decision algorithm in both cases we give a sound and complete inference system for a fragment of the language which is decidable in polynomial time. We finally show how to use the extended syntax to represent constrained delegation in SPKI.

  • 21.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Khakpour, Narges
    Nemati, Hamed
    Schwarz, Oliver
    Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel2013Conference paper (Refereed)
    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.

    Download full text (pdf)
    ccs13_dam_prosper_kernel_verification.pdf
  • 22.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nemati, Hamed
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Machine Code Verification of a Tiny ARM Hypervisor2013Conference paper (Refereed)
    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.

    Download full text (pdf)
    trusted13_dam_prosper_machine_code_verification.pdf
  • 23.
    Dam, Mads
    et al.
    KTH, Superseded Departments (pre-2005), Microelectronics and Information Technology, IMIT.
    Gurov, Dilian
    mu-calculus with explicit points and approximations2002In: Journal of logic and computation (Print), ISSN 0955-792X, E-ISSN 1465-363X, Vol. 12, no 2, p. 255-269Article in journal (Refereed)
    Abstract [en]

    We present a Gentzen-style sequent calculus for program verification which accommodates both model checking-like verification based on global state space exploration, and compositional reasoning. To handle the complexities arising from the presence of fixed-point formulas, programs with dynamically evolving architecture, and cut rules we use transition assertions, and introduce fixed-point approximants explicitly into the assertion language. We address, in a game-based manner, the semantical basis of this approach, as it applies to the entailment subproblem. Soundness and completeness results are obtained, and examples are shown illustrating some of the concepts.

  • 24.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Jacobs, B.
    Lundblad, Andreas
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Piessens, F.
    Provably Correct Inline Monitoring for Multi-threaded Java-like Programs2010In: Journal of Computer Security, ISSN 0926-227X, E-ISSN 1875-8924, Vol. 18, no 1, p. 37-59Article in journal (Other (popular science, discussion, etc.))
    Abstract [en]

    Inline reference monitoring is a powerful technique to enforce security policies on untrusted programs. The security-by-contract paradigm proposed by the EU FP6 S 3 MS project uses policies, monitoring, and monitor inlining to secure third-party applications running on mobile devices. The focus of this paper is on multi-threaded Java bytecode. An important consideration is that inlining should interfere with the client program only when mandated by the security policy. In a multithreaded setting, however, this requirement turns out to be problematic. Generally, inliners use locks to control access to shared resources such as an embedded monitor state. This will interfere with application program non-determinism due to Java's relaxed memory consistency model, and rule out the transparency property, that all policy-adherent behaviour of an application program is preserved under inlining. In its place we propose a notion of strong conservativity, to formalise the property that the inliner can terminate the client program only when the policy is about to be violated. An example inlining algorithm is given and proved to be strongly conservative. Finally, benchmarks are given for four example applications studied in the S 3 MS project.

  • 25.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Jacobs, B.
    Lundblad, Andreas
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Piessens, F.
    Security monitor inlining and certification for multithreaded Java2015In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 25, no 3, p. 528-565Article in journal (Refereed)
    Abstract [en]

    Security monitor inlining is a technique for security policy enforcement whereby monitor functionality is injected into application code in the style of aspect-oriented programming. The intention is that the injected code enforces compliance with the policy (security), and otherwise interferes with the application as little as possible (conservativity and transparency). Such inliners are said to be correct. For sequential Java-like languages, inlining is well understood, and several provably correct inliners have been proposed. For multithreaded Java one difficulty is the need to maintain a shared monitor state. We show that this problem introduces fundamental limitations in the type of security policies that can be correctly enforced by inlining. A class of race-free policies is identified that precisely characterizes the inlineable policies by showing that inlining of a policy outside this class is either not secure or not transparent, and by exhibiting a concrete inliner for policies inside the class which is secure, conservative and transparent. The inliner is implemented for Java and applied to a number of practical application security policies. Finally, we discuss how certification in the style of proof-carrying code could be supported for inlined programs by using annotations to reduce a potentially complex verification problem for multithreaded Java bytecode to sequential verification of just the inlined code snippets.

  • 26.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Jacobs, Bart
    Lundblad, Andreas
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Piessens, Frank
    Security Monitor Inlining for Multithreaded Java2009In: ECOOP 2009: OBJECT-ORIENTED PROGRAMMING / [ed] Drossopoulou S, 2009, Vol. 5653, p. 546-569Conference paper (Refereed)
    Abstract [en]

    Program monitoring is a well-established and efficient approach to security policy enforcement. An implementation of program monitoring that is particularly appealing for application-level policy enforcement is monitor inlining: the application is rewritten to push monitoring and policy enforcement code into the application itself. The intention is that the inserted code enforces compliance with the policy (security), and otherwise interferes with the application as little as possible (conservativity and transparency). For sequential Java-like languages, provably correct inlining algorithms have been proposed, but for the multithreaded setting, this is still an open problem. We show that no inliner for multithreaded Java can be both secure and transparent. It is however possible to identify a broad class of policies for which all three correctness criteria can be obtained. We propose an inliner that is correct for such policies, implement it for Java, and show that it is practical by reporting on some benchmarks.

  • 27.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Le Guernic, Gurvan
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Lundblad, Andreas
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    TreeDroid: A tree automaton based approach to enforcing data processing policies2012In: CCS '12 Proceedings of the 2012 ACM conference on Computer and communications security, ACM , 2012, p. 894-905Conference paper (Refereed)
    Abstract [en]

    Current approaches to security policy monitoring are based on linear control flow constraints such as runQuery may be evaluated only after sanitize. However, realistic security policies must be able to conveniently capture data flow constraints as well. An example is a policy stating that arguments to the function runQuery must be either constants, outputs of a function sanitize, or concatenations of any such values. We present a novel approach to security policy monitoring that uses tree automata to capture constraints on the way data is processed along an execution. We present a λ-calculus based model of the framework, investigate some of the models meta-properties, and show how it can be implemented using labels corresponding to automaton states to reflect the computational histories of each data item. We show how a standard denotational semantics induces the expected monitoring regime on a simple "while" language. Finally we implement the framework for the Dalvik VM using TaintDroid as the underlying data flow tracking mechanism, and evaluate its functionality and performance on five case studies.

  • 28.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Lundblad, Andreas
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    A proof carrying code framework for inlined reference monitors in java bytecode2010Report (Refereed)
    Abstract [en]

    We propose a light-weight approach for certification of monitor inlining for sequential Java bytecode using proof-carrying code. The goal is to enable the use of monitoring for quality assurance at development time, while minimizing the need for post-shipping code rewrites as well as changes to the end-host TCB. Standard automaton-based security policies express constraints on allowed API call/return sequences. Proofs are represented as JML-style program annotations. This is adequate in our case as all proofs generated in our framework are recognized in time polynomial in the size of the program. Policy adherence is proved by comparing the transitions of an inlined monitor with those of a trusted "ghost" monitor represented using JML-style annotations. At time of receiving a program with proof annotations, it is sufficient for the receiver to plug in its own trusted ghost monitor and check the resulting verification conditions, to verify that inlining has been performed correctly, of the correct policy. We have proved correctness of the approach at the Java bytecode level and formalized the proof of soundness in Coq. An implementation, including an application loader running on a mobile device, is available, and we conclude by giving benchmarks for two sample applications.

  • 29.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Decentralized Adaptive Power Control for Process NetworksManuscript (preprint) (Other academic)
    Abstract [en]

    Mobility and location transparency of distributed objects enable efficient resource allocation in networks, and can be effectively realized at the language level using location independent routing. However, the benefits of mobility are restricted by the available resources, e.g., in the form of processing nodes, which may be too few or too many to suit an application. To continually meet an application developer's requirements on computational task throughput, and an infrastructure provider's requirements on energy usage, the network itself must be able to adapt. In this paper, we consider fault-free networks of nodes connected point-to-point by asynchronous message passing channels, and propose a protocol for shutdown of nodes that preserves the integrity of distributed objects. This protocol enables decentralized power control, where nodes are turned on and off in response to computational requirements. We analyze the protocol both by verifying a restricted version in the model checker Spin, and by formulating a transition system model and proving properties by induction in that model for networks of arbitrary size. We define a protocol extension that, while using only a node's neighborhood-local information, is sufficient to ensure networks remain connected after node shutdown, and outline more complex, general local criteria. Finally, we discuss heuristics for node-local decision making on initiating a shutdown process, to meet adaptability requirements.

  • 30.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Efficient and Fully Abstract Routing of Futures in Object Network OverlaysManuscript (preprint) (Other academic)
    Abstract [en]

    In distributed object systems, it is desirable to enable migration of objects between locations, e.g., in order to support efficient resource allocation. Existing approaches build complex routing infrastructures to handle object-to-object communication, typically on top of IP, using, e.g., message forwarding chains or centralized object location servers. These solutions are costly and problematic in terms of efficiency, overhead, and correctness. We show how location independent routing can be used to implement object overlays with complex messaging behavior in a sound, fully abstract, and efficient way, on top of an abstract network of processing nodes connected point-to-point by asynchronous channels. We consider a distributed object language with futures, essentially lazy return values. Futures are challenging in this context due to the strong global consistency requirements they impose. The key conclusion is that execution in a decentralized, asynchronous network can preserve the standard, network-oblivious behavior of objects with futures, in the sense of contextual equivalence. To the best of our knowledge, this is the first such result in the literature. We also believe the proposed execution model may be of interest in its own right in the context of large-scale distributed computing.

    Download full text (pdf)
    fulltext
  • 31.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Efficient and fully abstract routing of futures in object network overlays2013In: AGERE! 2013 - Proceedings of the 2013 ACM Workshop on Programming Based on Actors, Agents, and Decentralized Control, Association for Computing Machinery (ACM), 2013, p. 49-59Conference paper (Refereed)
    Abstract [en]

    In distributed object systems, it is desirable to enable migration of objects between locations, e.g., in order to support efficient resource allocation. Existing approaches build complex routing infrastructures to handle object-to-object communication, typically on top of IP, using, e.g., message forwarding chains or centralized object location servers. These solutions are costly and problematic in terms of efficiency, overhead, and correctness. We show how location independent routing can be used to implement object overlays with complex messaging behavior in a sound, fully abstract, and efficient way, on top of an abstract network of processing nodes connected point-to-point by asynchronous channels. We consider a distributed object language with futures, essentially lazy return values. Futures are challenging in this context due to the global consistency requirements they impose. The key conclusion is that execution in a decentralized, asynchronous network can preserve the standard, network-oblivious behavior of objects with futures, in the sense of contextual equivalence. To the best of our knowledge, this is the first such result in the literature. We also believe the proposed execution model may be of interest in its own right in the context of large-scale distributed computing.

  • 32.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Location independent routing in process network overlays2014In: Proceedings - 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014, IEEE Computer Society, 2014, p. 715-724Conference paper (Refereed)
    Abstract [en]

    In distributed computing, location transparency - the decoupling of objects, tasks, and virtual machines from their physical location - is desirable in that it can simplify application development and management, and enable load balancing and efficient resource allocation. Many existing systems for location transparency are built on top of TCP/IP. We argue that addressing mobile objects in terms of the host where they temporarily reside may not be the best design decision. When objects can migrate, it becomes necessary to use a dedicated routing infrastructure to deliver inter-object messages, such as location servers or forwarding chains. This incurs high costs in terms of complexity, overhead, and latency. In this paper, we defer object overlay routing to an underlying networking layer, by assuming a location independent routing scheme in place of TCP/IP. In this scheme, messages are directed to destinations determined by flat identifiers instead of IP addresses. Consequently, messages are delivered directly to a recipient object, instead of a possibly out-of-date location. We explore the scheme in the context of a small object-based language with asynchronous message passing, in the style of core Erlang. We provide a standard, network-oblivious operational semantics of this language, and a network-aware semantics which takes many aspects of distribution and message routing into account. The main result is that execution of a program on top of an abstract network of processing nodes connected by asynchronous point-to-point communication channels preserves the network-oblivious behavior in a sound and fully abstract way, in the sense of contextual equivalence. This is a novel and strong result for such a low-level model. Previous work has addressed distributed implementations only in terms of fully connected TCP underlays. But in this setting, contextual equivalence is typically too strong, due to the need for locking to resolve preemption arising from object mobility.

  • 33.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Location Independent Routing in Process Network Overlays2014In: Service Oriented Computing and Applications, ISSN 1863-2386, E-ISSN 1863-2394, no Special Issue, p. 1-25Article in journal (Other academic)
    Abstract [en]

    In distributed computing, location transparency - the decoupling of objects, tasks, and virtual machines from their physical location - is desirable in that it can simplify application development and management, and enable load balancing and efficient resource allocation. Many existing systems for location transparency are built on top of TCP/IP. We argue that addressing mobile objects in terms of the host where they temporarily reside may not be the best design decision. When objects can migrate, it becomes necessary to use a dedicated routing infrastructure to deliver inter-object messages, such as location servers or forwarding chains. This incurs high costs in terms of complexity, overhead, and latency. In this paper, we defer object overlay routing to an underlying networking layer, by assuming a location independent routing scheme in place of TCP/IP. In this scheme, messages are directed to destinations determined by flat identifiers instead of IP addresses. Consequently, messages are delivered directly to a recipient object, instead of a possibly out-of-date location. We explore the scheme in the context of a small object-based language with asynchronous message passing, in the style of core Erlang. We provide a standard, network-oblivious operational semantics of this language, and a network-aware semantics which takes many aspects of distribution and message routing into account. The main result is that execution of a program on top of an abstract network of processing nodes connected by asynchronous point-to-point communication channels preserves the network-oblivious behavior in a sound and fully abstract way, in the sense of contextual equivalence. This is a novel and strong result for such a low-level model. Previous work has addressed distributed implementations only in terms of fully connected TCP underlays. But in this setting, contextual equivalence is typically too strong, due to the need for locking to resolve preemption arising from object mobility.

  • 34.
    Dam, Mads
    et al.
    KTH, School of Information and Communication Technology (ICT), Microelectronics and Information Technology, IMIT.
    Stadler, Rolf
    KTH, School of Information and Communication Technology (ICT), Microelectronics and Information Technology, IMIT.
    A Generic Protocol for Network State Aggregation2005Conference paper (Refereed)
    Abstract [en]

    Aggregation functions, which compute global parameters, such as the sum, minimum or average of local device variables, are needed for many network monitoring and management tasks. As networks grow larger and become more dynamic, it is crucial to compute these functions in a scalable and robust manner. To this end, we have developed GAP (Generic Aggregation Protocol), a novel protocol that computes aggregates of device variables for network management purposes. GAP supports continuous estimation of aggregates in a network where local state variables and the network graph may change. Aggregates are computed in a decentralized way using an aggregation tree. We have performed a functional evaluation of GAP in a simulation environment and have identied conguration choices that potentially allow us to control the performance characteristics of the protocol.

  • 35.
    Dong, Ning
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Refinement-Based Verification of Device-to-Device Information Flow2021In: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021, TU Wien Academic Press , 2021Conference paper (Refereed)
    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.

    Download full text (pdf)
    fulltext
  • 36.
    Dong, Ning
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Lööw, Andreas
    Imperial College London.
    Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor2023In: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 / [ed] Alexander Nadel; Kristin Yvonne Rozier, TU Wien Academic Press , 2023Conference paper (Refereed)
    Abstract [en]

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

  • 37.
    Dong, Ning
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Lööw, Andreas
    Imperial College London.
    Information Flow Analysis of a Verified In-Order Pipelined ProcessorManuscript (preprint) (Other academic)
    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.

    Download full text (pdf)
    fulltext
  • 38.
    Fetahi, Wuhib
    et al.
    KTH, School of Electrical Engineering (EES), Communication Networks.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Stadler, Rolf
    KTH, School of Electrical Engineering (EES), Communication Networks.
    Alexander, Clemm
    Cisco Systems, San Jose, CA USA.
    Robust Monitoring of Network-wide Aggregates through Gossiping2009In: IEEE Transactions on Network and Service Management, ISSN 1932-4537, E-ISSN 1932-4537, Vol. 6, no 2, p. 95-109Article in journal (Refereed)
    Abstract [en]

    We investigate the use of gossip protocols for continuousmonitoring of network-wide aggregates under crash failures.Aggregates are computed from local management variablesusing functions such as SUM, MAX, or AVERAGE. For this typeof aggregation, crash failures offer a particular challenge dueto the problem of mass loss, namely, how to correctly accountfor contributions from nodes that have failed. In this paper wegive a partial solution. We present G-GAP, a gossip protocolfor continuous monitoring of aggregates, which is robust againstfailures that are discontiguous in the sense that neighboringnodes do not fail within a short period of each other. We giveformal proofs of correctness and convergence, and we evaluatethe protocol through simulation using real traces. The simulationresults suggest that the design goals for this protocol have beenmet. For instance, the tradeoff between estimation accuracyand protocol overhead can be controlled, and a high estimationaccuracy (below some 5% error in our measurements) is achievedby the protocol, even for large networks and frequent nodefailures. Further, we perform a comparative assessment of GGAPagainst a tree-based aggregation protocol using simulation.Surprisingly, we find that the tree-based aggregation protocolconsistently outperforms the gossip protocol for comparativeoverhead, both in terms of accuracy and robustness.

    Download full text (pdf)
    fulltext
  • 39. Giambiagi, P.
    et al.
    Dam, Mads
    KTH, Superseded Departments (pre-2005), Computer and Systems Sciences, DSV.
    On the secure implementation of security protocols2004In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 50, no 3-Jan, p. 73-99Article in journal (Refereed)
    Abstract [en]

    We consider the problem of implementing a security protocol in such a manner that secrecy of sensitive data is not jeopardized. Implementation is assumed to take place in the context of an API that provides standard cryptography and communication services. Given a dependency specification, stating how API methods can produce and consume secret information, we propose an information flow property based on the idea of invariance under perturbation, relating observable changes in output to corresponding changes in input. Besides the information flow condition itself, the main contributions of the paper are results relating the admissibility property to a direct flow property in the special case of programs which branch on secrets only in cases permitted by the dependency rules. These results are used to derive an unwinding theorem, reducing a behavioural correctness check (strong bisimulation) to an invariant.

  • 40.
    Guanciale, Roberto
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Balliu, Musard
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis2020In: CCS '20: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications, Association for Computing Machinery (ACM) , 2020Conference paper (Refereed)
    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.  

  • 41.
    Guanciale, Roberto
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Baumann, C.
    Buiras, Pablo
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Nemati, H.
    A Case Study in Information Flow Refinement for Low Level Systems2022In: The Logic of Software. A Tasting Menu of Formal Methods, Springer Nature , 2022, p. 54-79Chapter in book (Other academic)
    Abstract [en]

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

  • 42.
    Guanciale, Roberto
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nemati, Hamed
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Baumann, Christoph
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures2016In: Proceedings - 2016 IEEE Symposium on Security and Privacy, SP 2016, Institute of Electrical and Electronics Engineers (IEEE), 2016, p. 38-55Conference paper (Refereed)
    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.

    Download full text (pdf)
    fulltext
  • 43.
    Guanciale, Roberto
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nemati, Hamed
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Baumann, Christoph
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Provably secure memory isolation for Linux on ARM2016In: Journal of Computer Security, ISSN 0926-227X, E-ISSN 1875-8924, Vol. 24, no 6, p. 793-837Article in journal (Refereed)
    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.

    Download full text (pdf)
    fulltext
  • 44. Guelev, D
    et al.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    An epistemic predicate CTL* for finite control pi-processes2011In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 278, no 1, p. 229-243Article in journal (Refereed)
    Abstract [en]

    We examine model checking of finite control π-calculus processes against specifications in epistemic predicate CTL*. In contrast to branching time settings such as CTL or the modal μ-calculus, the general problem, even for LTL, is undecidable, essentially because a process can use the environment as unbounded storage. To circumvent this problem attention is restricted to closed processes for which internal communication along a given set of known channels is observable. This allows to model processes operating in a suitably memory-bounded environment. We propose an epistemic predicate full CTL* with perfect recall which is interpreted on the computation trees defined by such finite control π-calculus processes. We demonstrate the decidability of model-checking by a reduction to the decidability of validity in quantified full propositional CTL*.

  • 45.
    Jónsson, Kristjan Valur
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Towards Flexible and Secure Distributed Aggregation2010In: MECHANISMS FOR AUTONOMOUS MANAGEMENT OF NETWORKS AND SERVICES / [ed] Stiller, B; DeTruck, F, 2010, Vol. 6155, p. 159-162Conference paper (Refereed)
    Abstract [en]

    Distributed aggregation algorithms are important in many present and future computing applications. However, after a decade of research, there are still numerous open questions regarding the security of this important class of algorithms. We intend to address some of these questions, mainly those regarding resilience against active attackers, whose aim is to compromise the integrity of the aggregate computation. Our work is currently in its initial stages, but we have identified promising research leads, which we present in this paper.

  • 46.
    Khakpour, Narges
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Schwarz, Oliver
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties2013In: Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, Springer, 2013, p. 276-291Conference paper (Refereed)
    Abstract [en]

    In this paper, we formally verify security properties of the ARMv7 Instruction Set Architecture (ISA) for user mode executions. To obtain guarantees that arbitrary (and unknown) user processes are able to run isolated from privileged software and other user processes, instruction level noninterference and integrity properties are provided, along with proofs that transitions to privileged modes can only occur in a controlled manner. This work establishes a main requirement for operating system and hypervisor verification, as demonstrated for the PROSPER separation kernel. The proof is performed in the HOL4 theorem prover, taking the Cambridge model of ARM as basis. To this end, a proof tool has been developed, which assists the verification of relational state predicates semi-automatically.

    Download full text (pdf)
    ARM_ISA_verification_Khakpour_author_version.pdf
  • 47.
    Kreitz, Gunnar
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Wikström, Douglas
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Practical Private Information Aggregation in Large Networks2012In: Information Security Technology For Applications, Springer Berlin/Heidelberg, 2012, p. 89-103Conference paper (Refereed)
    Abstract [en]

    Emerging approaches to network monitoring involve large numbers of agents collaborating to produce performance or security related statistics on huge, partial mesh networks. The aggregation process often involves security or business-critical information which network providers are generally unwilling to share without strong privacy protection. We present efficient and scalable protocols for privately computing a large range of aggregation functions based on addition, disjunction, and max/min. For addition, we give a protocol that is information-theoretically secure against a passive adversary, and which requires only one additional round compared to non-private protocols for computing sums. For disjunctions, we present both a computationally secure, and an information-theoretically secure solution. The latter uses a general composition approach which executes the sum protocol together with a standard multi-party protocol for a complete subgraph of ``trusted servers''. This can be used, for instance, when a large network can be partitioned into a smaller number of provider domains.

  • 48. Krishnamurthy, Supriya
    et al.
    Ardelius, John
    Aurell, Erik
    KTH, School of Computer Science and Communication (CSC), Computational Biology, CB. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Stadler, Rolf
    KTH, School of Electrical Engineering (EES), Communication Networks. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Wuhib, Fetahi Zebenigus
    KTH, School of Electrical Engineering (EES), Communication Networks. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Brief Announcement: The Accuracy of Tree-based Counting in Dynamic Networks2010In: PODC 2010: PROCEEDINGS OF THE 2010 ACM SYMPOSIUM ON PRINCIPLES OF DISTRIBUTED COMPUTING, NEW YORK: ASSOC COMPUTING MACHINERY , 2010, p. 291-292Conference paper (Refereed)
    Abstract [en]

    We study a simple Bellman-Ford-like protocol which performs network size estimation over a tree-shaped overlay. A continuous time Markov model is constructed which allows key protocol characteristics to be estimated under churn, including the expected number of nodes at a given (perceived) distance to the root and, for each such node, the expected (perceived) size of the subnetwork rooted at that node. We validate the model by simulations, using a range of network sizes, node degrees, and churn-to-protocol rates, with convincing results.

  • 49.
    Lindner, Andreas
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Guanciale, Roberto
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Proof-Producing Symbolic Execution for Binary Code VerificationManuscript (preprint) (Other academic)
  • 50.
    Lundberg, Didrik
    et al.
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS. Saab AB.
    Guanciale, Roberto
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Lindner, Andreas
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
    Hoare-Style Logic for Unstructured Programs2020In: Software Engineering and Formal Methods / [ed] Frank de Boer, Antonio Cerone, Cham: Springer Nature , 2020, p. 193-213Conference paper (Refereed)
    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.

    Download full text (pdf)
    fulltext
12 1 - 50 of 67
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf