Publications by Roberto Guanciale
Peer reviewed
Articles
[1]
A. Alshnakat et al., "HOL4P4: Mechanized Small-Step Semantics for P4," Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA1, 2024.
[2]
J. K. Larsen et al., "P4R-Type : A Verified API for P4 Control Plane Programs," Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, 2023.
[3]
A. Bocci et al., "Secure Partitioning of Cloud Applications, with Cost Look-Ahead," Future Internet, vol. 15, no. 7, 2023.
[4]
M. Wiggberg et al., "Effective Reskilling of Foreign-Born People at Universities-The Software Development Academy," IEEE Access, vol. 10, pp. 24556-24565, 2022.
[5]
A. Coto, R. Guanciale and E. Tuosto, "An abstract framework for choreographic testing," The Journal of logical and algebraic methods in programming, vol. 123, 2021.
[6]
R. Guanciale and E. Tuosto, "PomCho : Atool chain for choreographic design," Science of Computer Programming, vol. 202, 2021.
[7]
J. Haglund and R. Guanciale, "Trustworthy isolation of DMA devices," Journal of Banking and Financial Technology, 2020.
[8]
R. Guanciale and E. Tuosto, "Realisability of pomsets," The Journal of logical and algebraic methods in programming, vol. 108, pp. 69-89, 2019.
[9]
A. Lindner, R. Guanciale and R. Metere, "TrABin : Trustworthy analyses of binaries," Science of Computer Programming, vol. 174, pp. 72-89, 2019.
[10]
T. Emilio and R. Guanciale, "Semantics of global view of choreographies," Journal of Logic and Algebraic Programming, vol. 95, 2017.
[11]
R. Guanciale et al., "Provably secure memory isolation for Linux on ARM," Journal of Computer Security, vol. 24, no. 6, pp. 793-837, 2016.
[12]
R. Guanciale, D. Gurov and P. Laud, "Business process engineering and secure multiparty computation," Cryptology and Information Security Series, vol. 13, pp. 129-149, 2015.
[13]
H. Chfouka, A. Corradini and R. Guanciale, "Classification techniques for conformance and performance checking in process analysis," CEUR Workshop Proceedings, vol. 1101, pp. 21-30, 2013.
Conference papers
[14]
T. Marinaro et al., "Beyond Over-Protection : A Targeted Approach to Spectre Mitigation and Performance Optimization," in ACM AsiaCCS 2024 - Proceedings of the 19th ACM Asia Conference on Computer and Communications Security, 2024, pp. 203-216.
[15]
M. Soloviev, M. Balliu and R. Guanciale, "Security Properties through the Lens of Modal Logic," in 2024 IEEE 37th computer security foundations symposium, CSF 2024, 2024, pp. 340-355.
[16]
N. Dong et al., "Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor," in Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023, 2023.
[17]
J. Haglund and R. Guanciale, "Formally Verified Isolation of DMA," in Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022, 2022.
[18]
K. Palmskog et al., "Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution," in Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022, 2022, pp. 129-138.
[19]
A. Alshnakat et al., "HOL4P4 : Semantics for a Verified Data Plane," in EuroP4 2022 : Proceedings of the 5th International Workshop on P4 in Europe, Part of CoNEXT 2022, 2022, pp. 39-45.
[20]
A. Bocci et al., "Secure Partitioning of Composite Cloud Applications," in Service-Oriented and Cloud Computing, 2022, pp. 47-64.
[21]
R. Guanciale, N. Paladi and A. Vahidi, "SoK : Confidential Quartet - Comparison of Platforms for Virtualization-Based Confidential Computing," in 2022 IEEE international symposium on secure and private execution environment design (SEED 2022), 2022, pp. 109-120.
[22]
C. Baumann et al., "On Compositional Information Flow Aware Refinement," in 2021 IEEE 34Th Computer Security Foundations Symposium (CSF 2021), 2021, pp. 17-32.
[23]
N. Dong, R. Guanciale and M. Dam, "Refinement-Based Verification of Device-to-Device Information Flow," in Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021, 2021.
[24]
P. Buiras et al., "Validation of side-channel models via observation refinement," in Proceedings of the Annual International Symposium on Microarchitecture, MICRO, 2021, pp. 578-591.
[25]
A. Coto, R. Guanciale and E. Tuosto, "Choreographic development of message-passing applications : a tutorial," in Lecture Notes in Computer Science book series, 2020, pp. 20-36.
[26]
D. Lundberg et al., "Hoare-Style Logic for Unstructured Programs," in Software Engineering and Formal Methods, 2020, pp. 193-213.
[27]
R. Guanciale, M. Balliu and M. Dam, "InSpectre : Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis," in CCS '20: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications, 2020.
[28]
A. Coto, R. Guanciale and E. Tuosto, "On Testing Message-Passing Components," in Leveraging Applications of Formal Methods, Verification and Validation, 2020, pp. 22-38.
[29]
H. Nemati et al., "Validation of Abstract Side-Channel Models for Computer Architectures," in Lecture Notes in Computer Science book series, 2020, pp. 225-248.
[30]
R. Guanciale, "DiRPOMS: Automatic Checker of Distributed Realizability of POMSets," in COORDINATION 2019: Coordination Models and Languages, 2019.
[31]
J. Haglund and R. Guanciale, "Trustworthy Isolation of DMA Enabled Devices," in 15th International Conference on Information Systems Security, ICISS 2019, 2019, pp. 35-55.
[32]
H. Nemati et al., "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, 2018, pp. 109-133.
[33]
R. Guanciale, "Protecting Instruction Set Randomization from Code Reuse Attacks," in 23rd Nordic Conference on Secure IT Systems, NordSec 2018, 2018, pp. 421-436.
[34]
R. Guanciale and E. Tuosto, "Realisability of pomsets via communicating automata," in Electronic Proceedings in Theoretical Computer Science, EPTCS, 2018, pp. 37-51.
[35]
R. Metere, A. Lindner and R. Guanciale, "Sound transpilation from binary to machine-independent code," in 20th Brazilian Symposium on Formal Methods, SBMF 2017, 2017, pp. 197-214.
[36]
R. Guanciale and E. Tuosto, "An Abstract Semantics of the Global View of Choreographies," in Proceedings 9th Interaction and Concurrency Experience, 2016.
[37]
R. Guanciale et al., "Cache Storage Channels : Alias-Driven Attacks and Verified Countermeasures," in Proceedings - 2016 IEEE Symposium on Security and Privacy, SP 2016, 2016, pp. 38-55.
[38]
R. Guanciale and D. Gurov, "Privacy preserving business process fusion," in International Workshops on Business Process Management Workshops, BPM 2014, 2015, pp. 96-101.
[39]
D. Gurov, P. Laud and R. Guanciale, "Privacy preserving business process matching," in 2015 13th Annual Conference on Privacy, Security and Trust, 2015, pp. 36-43.
[40]
H. Nemati et al., "Trustworthy Memory Isolation of Linux on Embedded Devices," in Trust and Trustworthy Computing, TRUST 2015, 2015, pp. 125-142.
[41]
H. Chfouka et al., "Trustworthy prevention of code injection in Linux on embedded devices," in 20th European Symposium on Research in Computer Security, ESORICS 2015, 2015, pp. 90-107.
[42]
H. Nemati, R. Guanciale and M. Dam, "Trustworthy virtualization of the ARMv7 memory subsystem," in 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015, 2015, pp. 578-589.
[43]
M. Balliu, M. Dam and R. Guanciale, "Automating Information Flow Analysis of Low Level Code," in Proceedings of CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA, 2014.
[44]
R. Guanciale, D. Gurov and P. Laud, "Private intersection of regular languages," in Privacy, Security and Trust (PST), 2014 Twelfth Annual International Conference on, 2014, pp. 112-120.
[45]
M. Dam et al., "Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel," in 2013 ACM SIGSAC Conference on Computer & Communications Security (CCS'13),November 4 - 8, 2013 Berlin, Germany, 2013.
[46]
M. Dam, R. Guanciale and H. Nemati, "Machine Code Verification of a Tiny ARM Hypervisor," in TrustED 13, November 4 2013, Berlin, Germany, 2013.
Non-peer reviewed
Conference papers
[47]
A. Coto, R. Guanciale and E. Tuosto, "An abstract framework for choreographic testing," in Electronic Proceedings in Theoretical Computer Science, EPTCS, 2020, pp. 43-60.
Chapters in books
[48]
R. Guanciale et al., "A Case Study in Information Flow Refinement for Low Level Systems," in The Logic of Software. A Tasting Menu of Formal Methods, : Springer Nature, 2022, pp. 54-79.
Other
[49]
H. Nemati et al., "Formal Analysis of Countermeasures against Cache Storage Side Channels," (Manuscript).
[50]
M. Balliu, M. Dam and R. Guanciale, "InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis.," (Manuscript).
[51]
N. Dong et al., "Information Flow Analysis of a Verified In-Order Pipelined Processor," (Manuscript).
[52]
A. Lindner, R. Guanciale and M. Dam, "Proof-Producing Symbolic Execution for Binary Code Verification," (Manuscript).
Latest sync with DiVA:
2024-11-18 00:14:11