Change search
Link to record
Permanent link

Direct link
BETA
Guanciale, Roberto
Publications (9 of 9) Show all publications
Guanciale, R. (2019). DiRPOMS: Automatic Checker of Distributed Realizability of POMSets. In: COORDINATION 2019: Coordination Models and Languages: . Paper presented at Coordination Models and Languages.
Open this publication in new window or tab >>DiRPOMS: Automatic Checker of Distributed Realizability of POMSets
2019 (English)In: COORDINATION 2019: Coordination Models and Languages, 2019Conference paper, Published paper (Refereed)
Abstract [en]

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

Keywords
Pomsets; Choreography; Realisability; CFSMs
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-261173 (URN)10.1007/978-3-030-22397-7_14 (DOI)2-s2.0-8506746149 (Scopus ID)
Conference
Coordination Models and Languages
Projects
Trustfull
Note

QC 20191209

Available from: 2019-10-02 Created: 2019-10-02 Last updated: 2019-12-09Bibliographically approved
Lindner, A., Guanciale, R. & Metere, R. (2019). TrABin: Trustworthy analyses of binaries. Science of Computer Programming, 174, 72-89
Open this publication in new window or tab >>TrABin: Trustworthy analyses of binaries
2019 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 174, p. 72-89Article in journal (Refereed) Published
Abstract [en]

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

Place, publisher, year, edition, pages
Elsevier, 2019
Keywords
Binary analysis, Formal verification, Proof producing analysis, Theorem proving
National Category
Computer Systems
Identifiers
urn:nbn:se:kth:diva-246462 (URN)10.1016/j.scico.2019.01.001 (DOI)000461533200003 ()2-s2.0-85060511323 (Scopus ID)
Projects
Trustfull
Note

QC 20190321

Available from: 2019-03-21 Created: 2019-03-21 Last updated: 2019-10-04Bibliographically approved
Nemati, H., Baumann, C., Guanciale, R. & Dam, M. (2018). Formal verification of integrity-Preserving countermeasures against cache storage side-channels. In: 7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018: . Paper presented at 7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018; Thessaloniki; Greece; 14 April 2018 through 20 April 2018 (pp. 109-133). Springer, 10804
Open this publication in new window or tab >>Formal verification of integrity-Preserving countermeasures against cache storage side-channels
2018 (English)In: 7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Springer, 2018, Vol. 10804, p. 109-133Conference paper, Published paper (Refereed)
Abstract [en]

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

Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10804
Keywords
Cache memory, Hardware, Network security, Hardware models, Information leakage, Low-level features, Security analysis, Software and hardwares, Storage channels, Verification condition, Verification methodology, Formal verification
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:kth:diva-227490 (URN)10.1007/978-3-319-89722-6_5 (DOI)000445805600005 ()2-s2.0-85045658183 (Scopus ID)9783319897219 (ISBN)
Conference
7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018; Thessaloniki; Greece; 14 April 2018 through 20 April 2018
Projects
trustfullcerces
Note

QC 20180516

QC 20181012

Available from: 2018-05-16 Created: 2018-05-16 Last updated: 2019-11-20Bibliographically approved
Guanciale, R. (2018). Protecting Instruction Set Randomization from Code Reuse Attacks. In: 23rd Nordic Conference on Secure IT Systems, NordSec 2018: . Paper presented at 28 November 2018 through 30 November 2018 (pp. 421-436). Springer Verlag
Open this publication in new window or tab >>Protecting Instruction Set Randomization from Code Reuse Attacks
2018 (English)In: 23rd Nordic Conference on Secure IT Systems, NordSec 2018, Springer Verlag , 2018, p. 421-436Conference paper, Published paper (Refereed)
Abstract [en]

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

Place, publisher, year, edition, pages
Springer Verlag, 2018
Series
Lecture Notes in Computer Science, ISSN 03029743, E-ISSN 1611-3349
Keywords
Code injection, Code-reuse attacks, Instruction Set Randomization, Cryptography, Hardware, Random access storage, Random processes, Code reuse, Hardware implementations, Hardware simulators, Instruction encoding, Instruction-set randomization, Random access, Codes (symbols)
National Category
Computer Engineering
Identifiers
urn:nbn:se:kth:diva-247459 (URN)10.1007/978-3-030-03638-6_26 (DOI)2-s2.0-85057419569 (Scopus ID)9783030036379 (ISBN)
Conference
28 November 2018 through 30 November 2018
Projects
trustfull
Note

QC 20191024

Available from: 2019-04-03 Created: 2019-04-03 Last updated: 2019-11-06Bibliographically approved
Guanciale, R. & Tuosto, E. (2018). Realisability of pomsets via communicating automata. In: Electronic Proceedings in Theoretical Computer Science, EPTCS: . Paper presented at 11th Interaction and Concurrency Experience, ICE 2018, Madrid, Spain, 20 June 2018 through 21 June 2018 (pp. 37-51). Open Publishing Association, 279
Open this publication in new window or tab >>Realisability of pomsets via communicating automata
2018 (English)In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association , 2018, Vol. 279, p. 37-51Conference paper, Published paper (Refereed)
Abstract [en]

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

Place, publisher, year, edition, pages
Open Publishing Association, 2018
Series
Electronic Proceedings in Theoretical Computer Science, EPTCS, ISSN 2075-2180 ; 279
National Category
Control Engineering
Identifiers
urn:nbn:se:kth:diva-241856 (URN)10.4204/EPTCS.279.6 (DOI)000465427700007 ()2-s2.0-85060051773 (Scopus ID)
Conference
11th Interaction and Concurrency Experience, ICE 2018, Madrid, Spain, 20 June 2018 through 21 June 2018
Projects
Trustfull
Note

QC 20190125

Available from: 2019-01-25 Created: 2019-01-25 Last updated: 2019-10-11Bibliographically approved
Nemati, H., Guanciale, R., Baumann, C. & Dam, M. (2017). Formal Analysis of Countermeasures against Cache Storage Side Channels. Paper presented at -.
Open this publication in new window or tab >>Formal Analysis of Countermeasures against Cache Storage Side Channels
2017 (English)Manuscript (preprint) (Other academic)
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-213405 (URN)
Conference
-
Note

QC 20170830

Available from: 2017-08-30 Created: 2017-08-30 Last updated: 2019-08-20Bibliographically approved
Emilio, T. & Guanciale, R. (2017). Semantics of global view of choreographies. Journal of Logic and Algebraic Programming, 95
Open this publication in new window or tab >>Semantics of global view of choreographies
2017 (English)In: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 95Article in journal (Refereed) Published
Abstract [en]

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

Keywords
Choreography, Communicating finite-state machines, Global graphs, Hypergraphs, Pomsets, Semantics
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:kth:diva-220700 (URN)10.1016/j.jlamp.2017.11.002 (DOI)000425079300002 ()2-s2.0-85043486051 (Scopus ID)
Note

QC 20180108

Available from: 2018-01-02 Created: 2018-01-02 Last updated: 2018-05-28Bibliographically approved
Metere, R., Lindner, A. & Guanciale, R. (2017). Sound transpilation from binary to machine-independent code. In: 20th Brazilian Symposium on Formal Methods, SBMF 2017: . Paper presented at 20th Brazilian Symposium on Formal Methods, SBMF 2017, Recife, Brazil, 29 November 2017 through 1 December 2017 (pp. 197-214). Springer, 10623
Open this publication in new window or tab >>Sound transpilation from binary to machine-independent code
2017 (English)In: 20th Brazilian Symposium on Formal Methods, SBMF 2017, Springer, 2017, Vol. 10623, p. 197-214Conference paper, Published paper (Refereed)
Abstract [en]

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

Place, publisher, year, edition, pages
Springer, 2017
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 10623
Keywords
Binary analysis, Formal verification, Proof producing analysis, Theorem proving
National Category
Embedded Systems
Identifiers
urn:nbn:se:kth:diva-219665 (URN)10.1007/978-3-319-70848-5_13 (DOI)2-s2.0-85035086144 (Scopus ID)9783319708478 (ISBN)
Conference
20th Brazilian Symposium on Formal Methods, SBMF 2017, Recife, Brazil, 29 November 2017 through 1 December 2017
Projects
trustfull
Note

QC 20171212

Available from: 2017-12-12 Created: 2017-12-12 Last updated: 2019-11-15Bibliographically approved
Guanciale, R. & Tuosto, E. (2016). An Abstract Semantics of the Global View of Choreographies. In: Proceedings 9th Interaction and Concurrency Experience: . Paper presented at ICE 2016. Open Publishing Association
Open this publication in new window or tab >>An Abstract Semantics of the Global View of Choreographies
2016 (English)In: Proceedings 9th Interaction and Concurrency Experience, Open Publishing Association , 2016Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Open Publishing Association, 2016
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-198183 (URN)10.4204/EPTCS.223.5 (DOI)000390324700006 ()2-s2.0-84992195831 (Scopus ID)
Conference
ICE 2016
Note

QC 20161219

Available from: 2016-12-13 Created: 2016-12-13 Last updated: 2018-01-13Bibliographically approved
Organisations

Search in DiVA

Show all publications