Ändra sökning
Länk till posten
Permanent länk

Direktlänk
BETA
Guanciale, Roberto
Publikationer (9 of 9) Visa alla publikationer
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.
Öppna denna publikation i ny flik eller fönster >>DiRPOMS: Automatic Checker of Distributed Realizability of POMSets
2019 (Engelska)Ingår i: COORDINATION 2019: Coordination Models and Languages, 2019Konferensbidrag, Publicerat paper (Refereegranskat)
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/).

Nyckelord
Pomsets; Choreography; Realisability; CFSMs
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
urn:nbn:se:kth:diva-261173 (URN)10.1007/978-3-030-22397-7_14 (DOI)2-s2.0-8506746149 (Scopus ID)
Konferens
Coordination Models and Languages
Projekt
Trustfull
Anmärkning

QC 20191209

Tillgänglig från: 2019-10-02 Skapad: 2019-10-02 Senast uppdaterad: 2019-12-09Bibliografiskt granskad
Lindner, A., Guanciale, R. & Metere, R. (2019). TrABin: Trustworthy analyses of binaries. Science of Computer Programming, 174, 72-89
Öppna denna publikation i ny flik eller fönster >>TrABin: Trustworthy analyses of binaries
2019 (Engelska)Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 174, s. 72-89Artikel i tidskrift (Refereegranskat) 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.

Ort, förlag, år, upplaga, sidor
Elsevier, 2019
Nyckelord
Binary analysis, Formal verification, Proof producing analysis, Theorem proving
Nationell ämneskategori
Datorsystem
Identifikatorer
urn:nbn:se:kth:diva-246462 (URN)10.1016/j.scico.2019.01.001 (DOI)000461533200003 ()2-s2.0-85060511323 (Scopus ID)
Projekt
Trustfull
Anmärkning

QC 20190321

Tillgänglig från: 2019-03-21 Skapad: 2019-03-21 Senast uppdaterad: 2019-10-04Bibliografiskt granskad
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
Öppna denna publikation i ny flik eller fönster >>Formal verification of integrity-Preserving countermeasures against cache storage side-channels
2018 (Engelska)Ingår i: 7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Springer, 2018, Vol. 10804, s. 109-133Konferensbidrag, Publicerat paper (Refereegranskat)
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. 

Ort, förlag, år, upplaga, sidor
Springer, 2018
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10804
Nyckelord
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
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
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)
Konferens
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
Projekt
trustfullcerces
Anmärkning

QC 20180516

QC 20181012

Tillgänglig från: 2018-05-16 Skapad: 2018-05-16 Senast uppdaterad: 2019-11-20Bibliografiskt granskad
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
Öppna denna publikation i ny flik eller fönster >>Protecting Instruction Set Randomization from Code Reuse Attacks
2018 (Engelska)Ingår i: 23rd Nordic Conference on Secure IT Systems, NordSec 2018, Springer Verlag , 2018, s. 421-436Konferensbidrag, Publicerat paper (Refereegranskat)
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. 

Ort, förlag, år, upplaga, sidor
Springer Verlag, 2018
Serie
Lecture Notes in Computer Science, ISSN 03029743, E-ISSN 1611-3349
Nyckelord
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)
Nationell ämneskategori
Datorteknik
Identifikatorer
urn:nbn:se:kth:diva-247459 (URN)10.1007/978-3-030-03638-6_26 (DOI)2-s2.0-85057419569 (Scopus ID)9783030036379 (ISBN)
Konferens
28 November 2018 through 30 November 2018
Projekt
trustfull
Anmärkning

QC 20191024

Tillgänglig från: 2019-04-03 Skapad: 2019-04-03 Senast uppdaterad: 2019-11-06Bibliografiskt granskad
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
Öppna denna publikation i ny flik eller fönster >>Realisability of pomsets via communicating automata
2018 (Engelska)Ingår i: Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association , 2018, Vol. 279, s. 37-51Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Open Publishing Association, 2018
Serie
Electronic Proceedings in Theoretical Computer Science, EPTCS, ISSN 2075-2180 ; 279
Nationell ämneskategori
Reglerteknik
Identifikatorer
urn:nbn:se:kth:diva-241856 (URN)10.4204/EPTCS.279.6 (DOI)000465427700007 ()2-s2.0-85060051773 (Scopus ID)
Konferens
11th Interaction and Concurrency Experience, ICE 2018, Madrid, Spain, 20 June 2018 through 21 June 2018
Projekt
Trustfull
Anmärkning

QC 20190125

Tillgänglig från: 2019-01-25 Skapad: 2019-01-25 Senast uppdaterad: 2019-10-11Bibliografiskt granskad
Nemati, H., Guanciale, R., Baumann, C. & Dam, M. (2017). Formal Analysis of Countermeasures against Cache Storage Side Channels. Paper presented at -.
Öppna denna publikation i ny flik eller fönster >>Formal Analysis of Countermeasures against Cache Storage Side Channels
2017 (Engelska)Manuskript (preprint) (Övrigt vetenskapligt)
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
urn:nbn:se:kth:diva-213405 (URN)
Konferens
-
Anmärkning

QC 20170830

Tillgänglig från: 2017-08-30 Skapad: 2017-08-30 Senast uppdaterad: 2019-08-20Bibliografiskt granskad
Emilio, T. & Guanciale, R. (2017). Semantics of global view of choreographies. Journal of Logic and Algebraic Programming, 95
Öppna denna publikation i ny flik eller fönster >>Semantics of global view of choreographies
2017 (Engelska)Ingår i: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 95Artikel i tidskrift (Refereegranskat) 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.

Nyckelord
Choreography, Communicating finite-state machines, Global graphs, Hypergraphs, Pomsets, Semantics
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:kth:diva-220700 (URN)10.1016/j.jlamp.2017.11.002 (DOI)000425079300002 ()2-s2.0-85043486051 (Scopus ID)
Anmärkning

QC 20180108

Tillgänglig från: 2018-01-02 Skapad: 2018-01-02 Senast uppdaterad: 2018-05-28Bibliografiskt granskad
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
Öppna denna publikation i ny flik eller fönster >>Sound transpilation from binary to machine-independent code
2017 (Engelska)Ingår i: 20th Brazilian Symposium on Formal Methods, SBMF 2017, Springer, 2017, Vol. 10623, s. 197-214Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Springer, 2017
Serie
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 10623
Nyckelord
Binary analysis, Formal verification, Proof producing analysis, Theorem proving
Nationell ämneskategori
Inbäddad systemteknik
Identifikatorer
urn:nbn:se:kth:diva-219665 (URN)10.1007/978-3-319-70848-5_13 (DOI)2-s2.0-85035086144 (Scopus ID)9783319708478 (ISBN)
Konferens
20th Brazilian Symposium on Formal Methods, SBMF 2017, Recife, Brazil, 29 November 2017 through 1 December 2017
Projekt
trustfull
Anmärkning

QC 20171212

Tillgänglig från: 2017-12-12 Skapad: 2017-12-12 Senast uppdaterad: 2019-11-15Bibliografiskt granskad
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
Öppna denna publikation i ny flik eller fönster >>An Abstract Semantics of the Global View of Choreographies
2016 (Engelska)Ingår i: Proceedings 9th Interaction and Concurrency Experience, Open Publishing Association , 2016Konferensbidrag, Publicerat paper (Refereegranskat)
Ort, förlag, år, upplaga, sidor
Open Publishing Association, 2016
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
urn:nbn:se:kth:diva-198183 (URN)10.4204/EPTCS.223.5 (DOI)000390324700006 ()2-s2.0-84992195831 (Scopus ID)
Konferens
ICE 2016
Anmärkning

QC 20161219

Tillgänglig från: 2016-12-13 Skapad: 2016-12-13 Senast uppdaterad: 2018-01-13Bibliografiskt granskad
Organisationer

Sök vidare i DiVA

Visa alla publikationer