Publications

[Extracted from DiVA, the publication database at KTH.]

Baumann, C.; Dam, M.; Guanciale, R.; Nemati, H. (2021):
On Compositional Information Flow Aware Refinement.
[Conference paper] 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021; 2021 IEEE 34Th Computer Security Foundations Symposium (CSF 2021) 17-32 [Details]
Dong, N.; Guanciale, R.; Dam, M. (2021):
Refinement-Based Verification of Device-to-Device Information Flow.
[Conference paper] Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021; Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 [Details]
Guanciale, R.; Balliu, M.; Dam, M. (2020):
InSpectre - Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis.
[Conference paper] CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, USA, November 9-13, 2020; CCS '20: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications [Details]
Lundberg, D.; Guanciale, R.; Lindner, A.; Dam, M. (2020):
Hoare-Style Logic for Unstructured Programs.
[Conference paper] 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020; Software Engineering and Formal Methods 193-213 [Details]
Baumann, C.; Schwarz, O.; Dam, M. (2019):
On the verification of system-level information flow properties for virtualized execution platforms.
Journal of Cryptographic Engineering 9: 243-261 [Details]
Costa, M.; Harrucksteiner, A.; Malusà, S.; Oggioni, N.; Sebastiani, A.; van Dam, B. (2018):
A future view on the Nakano district.
Report [Details]
Nemati, H.; Baumann, C.; Guanciale, R.; Dam, M. (2018):
Formal verification of integrity-Preserving countermeasures against cache storage side-channels.
[Conference paper] 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; 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 109-133 [Details]
Baumann, C.; Schwarz, O.; Dam, M. (2017):
Compositional Verification of Security Properties for Embedded Execution Platforms.
[Conference paper] PROOFS 2017. 6th International Workshop on Security Proofs for Embedded Systems; PROOFS 2017 1-16 [Details]
Nemati, H.; Guanciale, R.; Baumann, C.; Dam, M. (2017):
Formal Analysis of Countermeasures against Cache Storage Side Channels.
Manuscript (preprint) [Details]
Schwarz, O.; Dam, M. (2016):
Automatic Derivation of Platform Noninterference Properties.
[Conference paper] 14th International Conference on Software Engineering and Formal Methods, SEFM 2016 Held as Part of Conference on Software Technologies: Applications and Foundations, STAF 2016, Vienna, Austria, 4 July 2016 through 8 July 2016; Software Engineering and Formal Methods, Springer LNCS 9763 27-44 [Details]
Guanciale, R.; Nemati, H.; Baumann, C.; Dam, M. (2016):
Cache Storage Channels - Alias-Driven Attacks and Verified Countermeasures.
[Conference paper] 2016 IEEE Symposium on Security and Privacy, SP 2016, 23 May 2016 through 25 May 2016; Proceedings - 2016 IEEE Symposium on Security and Privacy, SP 2016 38-55 [Details]
Guanciale, R.; Nemati, H.; Dam, M.; Baumann, C. (2016):
Provably secure memory isolation for Linux on ARM.
Journal of Computer Security 24: 793-837 [Details]
Nemati, H.; Guanciale, R.; Dam, M. (2015):
Trustworthy virtualization of the ARMv7 memory subsystem.
[Conference paper] 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015; Pec pod Sněžkou; Czech Republic; 24 January 2015 through 29 January 2015; 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015 578-589 [Details]
Chfouka, H.; Nemati, H.; Guanciale, R.; Dam, M.; Ekdahl, P. (2015):
Trustworthy prevention of code injection in Linux on embedded devices.
[Conference paper] 20th European Symposium on Research in Computer Security, ESORICS 2015; Vienna; Austria; 20th European Symposium on Research in Computer Security, ESORICS 2015 90-107 [Details]
(2015):
Secure IT Systems - 20th Nordic Conference, NordSec 2015 Stockholm, Sweden, October 19-21, 2015 Proceedings.
Conference proceedings (editor) [Details]
Nemati, H.; Dam, M.; Guanciale, R.; Do, V.; Vahidi, A. (2015):
Trustworthy Memory Isolation of Linux on Embedded Devices.
[Conference paper] 8th International Conference on Trust and Trustworthy Computing (TRUST), AUG 24-26, 2015, Fdn Res & Technol Hellas, Inst Comp Sci, Heraklion, GREECE; Trust and Trustworthy Computing, TRUST 2015 125-142 [Details]
Dam, M.; Jacobs, B.; Lundblad, A.; Piessens, F. (2015):
Security monitor inlining and certification for multithreaded Java.
Mathematical Structures in Computer Science 25: 528-565 [Details]
Schwarz, O.; Dam, M. (2014):
Formal Verification of Secure User Mode Device Execution with DMA.
[Conference paper] 10th International Haifa Verification Conference, HVC 2014; Hardware and Software 236-251 [Details]
Balliu, M.; Dam, M.; Guanciale, R. (2014):
Automating Information Flow Analysis of Low Level Code.
[Conference paper] CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA; Proceedings of CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA [Details]
Dam, M.; Palmskog, K. (2014):
Location independent routing in process network overlays.
[Conference paper] 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014; Turin; Italy; 12 February 2014 through 14 February 2014; Proceedings - 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014 715-724 [Details]
Dam, M.; Palmskog, K. (2014):
Location Independent Routing in Process Network Overlays.
Service Oriented Computing and Applications Special Issue: 1-25 [Details]
Palmskog, K.; Dam, M.; Lundblad, A.; Jafari, A. (2013):
ABS-NET: Fully Decentralized Runtime Adaptation for Distributed Objects.
[Conference paper] The 6th Interaction and Concurrency Experience workshop, Florence, Italy, the 6th of June 2013; Proceedings 6th Interaction and Concurrency Experience 85-100 [Details]
Dam, M.; Palmskog, K. (2013):
Efficient and fully abstract routing of futures in object network overlays.
[Conference paper] 2013 3rd ACM Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE! 2013; Indianapolis, IN; United States; 27 October 2013 through 27 October 2013; AGERE! 2013 - Proceedings of the 2013 ACM Workshop on Programming Based on Actors, Agents, and Decentralized Control 49-59 [Details]
Khakpour, N.; Schwarz, O.; Dam, M. (2013):
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties.
[Conference paper] Certified Programs and Proofs (CPP); Certified Programs and Proofs 276-291 [Details]
Dam, M.; Guanciale, R.; Nemati, H. (2013):
Machine Code Verification of a Tiny ARM Hypervisor.
[Conference paper] TrustED 13, November 4 2013, Berlin, Germany; [Details]
Dam, M.; Guanciale, R.; Khakpour, N.; Nemati, H.; Schwarz, O. (2013):
Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel.
[Conference paper] 2013 ACM SIGSAC Conference on Computer & Communications Security (CCS'13),November 4 - 8, 2013 Berlin, Germany; [Details]
Dam, M.; Le Guernic, G.; Lundblad, A. (2012):
TreeDroid - A tree automaton based approach to enforcing data processing policies.
[Conference paper] 2012 ACM Conference on Computer and Communications Security, CCS 2012, 16 October 2012 through 18 October 2012, Raleigh, NC; CCS '12 Proceedings of the 2012 ACM conference on Computer and communications security 894-905 [Details]
Balliu, M.; Dam, M.; Le Guernic, G. (2012):
ENCOVER - Symbolic Exploration for Information Flow Security.
[Conference paper] 25th IEEE Computer Security Foundations Symposium (CSF), JUN 25-27, 2012, Cambridge, MA; 2012 IEEE 25th Computer Security Foundations Symposium (CSF) 30-44 [Details]
Kreitz, G.; Dam, M.; Wikström, D. (2012):
Practical Private Information Aggregation in Large Networks.
[Conference paper] 15th Nordic Conference on Secure IT Systems, NordSec 2010;Espoo;27 October 2010 through 29 October 2010; Information Security Technology For Applications 89-103 [Details]
Guelev, D.; Dam, M. (2011):
An epistemic predicate CTL* for finite control pi-processes.
Electronical Notes in Theoretical Computer Science 278: 229-243 [Details]
Balliu, M.; Dam, M.; Le Guernic, G. (2011):
Epistemic Temporal Logic for Information Flow Security.
[Conference paper] ACM SIGPLAN Sixth Workshop on Programming Languages and Analysis for Security (PLAS 2011). San Jose, USA. June 05 2011; In proc. of th 4e ACM SIGPLAN workshop on Programming Languages and Analysis for Security [Details]
Dam, M.; Lundblad, A. (2010):
A proof carrying code framework for inlined reference monitors in java bytecode.
Report [Details]
Dam, M.; Jacobs, B.; Lundblad, A.; Piessens, F. (2010):
Provably Correct Inline Monitoring for Multi-threaded Java-like Programs.
Journal of Computer Security 18: 37-59 [Details]
Palmskog, K.; Gonzalez Prieto, A.; Meirosu, C.; Stadler, R.; Dam, M. (2010):
Scalable Metadata-Directed Search in a Network of Information.
[Conference paper] 2010 Future Network and Mobile Summit; Florence; Italy; 16 June 2010 through 18 June 2010; Future Network and MobileSummit 2010 Conference Proceedings 5722376 [Details]
Raz, D.; Stadler, R.; Elster, C.; Dam, M. (2010):
In-Network Monitoring.
Chapter in book [Details]
Wuhib, F.; Dam, M.; Stadler, R. (2010):
A Gossiping Protocol for Detecting Global Threshold Crossings.
IEEE Transactions on Network and Service Management 7: 42-57 [Details]
Krishnamurthy, S.; Ardelius, J.; Aurell, E.; Dam, M.; Stadler, R.; Wuhib, F. (2010):
Brief Announcement: The Accuracy of Tree-based Counting in Dynamic Networks.
[Conference paper] 2010 ACM SYMPOSIUM ON PRINCIPLES OF DISTRIBUTED COMPUTING; PODC 2010 291-292 [Details]
Jónsson, K.; Dam, M. (2010):
Towards Flexible and Secure Distributed Aggregation.
[Conference paper] 4th International Conference on Autonomous Infrastructure Management and Security (AIMS 2010). Univ Zurich, Dept informat IFI, Commun Syst Grp, Zurich, SWITZERLAND. JUN 23-25, 2010; MECHANISMS FOR AUTONOMOUS MANAGEMENT OF NETWORKS AND SERVICES 159-162 [Details]
Cohen, M.; Dam, M.; Lomuscio, A.; Qu, H. (2009):
A data symmetry reduction technique for temporal-epistemic logic.
[Conference paper] 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009; Macao; China; 14 October 2009 through 16 October 2009; Automated Technology for Verification and Analysis 69-83 [Details]
Cohen, M.; Dam, M.; Lomuscio, A.; Russo, F. (2009):
Abstraction in Model Checking Multi-agent Systems.
[Conference paper] AAMAS '09, the 8th International Conference on Autonomous Agents and Multiagent Systems. Budapest, Hungary. May 10-15, 2009; AAMAS '09 Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems 710-717 [Details]
Cohen, M.; Lomuscio, A.; Dam, M.; Qu, H. (2009):
A symmetry reduction technique for model checking temporal epistemic logic.
[Conference paper] 21st Internation Joint Conference on Artifical Intelligence (IJCAI-09), Pasadena, CA, JUL 11-17, 2009; 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS 721-726 [Details]
Fetahi, W.; Dam, M.; Stadler, R.; Alexander, C. (2009):
Robust Monitoring of Network-wide Aggregates through Gossiping.
IEEE Transactions on Network and Service Management 6: 95-109 [Details]
Stadler, R.; Dam, M.; Gonzalez Prieto, A.; Wuhib, F. (2009):
Decentralized real-time monitoring of network-wide aggregates.
[Conference paper] 2nd Workshop on Large-Scale Distributed Systems and Middleware, LADIS'08; Yorktown Heights; Proceedings of the 2nd Workshop on Large-Scale Distributed Systems and Middleware [Details]
Wuhib, F.; Stadler, R.; Dam, M. (2009):
Gossiping for Threshold Detection.
[Conference paper] IFIP/IEEE International Symposium on Integrated Network Management (IM 2009) New York, NY, JUN 01-05, 2009; 2009 IFIP/IEEE INTERNATIONAL SYMPOSIUM ON INTEGRATED NETWORK MANAGEMENT (IM 2009) VOLS 1 AND 2 259-266 [Details]
Dam, M.; Jacobs, B.; Lundblad, A.; Piessens, F. (2009):
Security Monitor Inlining for Multithreaded Java.
[Conference paper] 23rd European Conference on Object-Oriented Programming (ECOOP 2009), Genoa, ITALY, JUL 06-10, 2009; ECOOP 2009 546-569 [Details]
Aktug, I.; Dam, M.; Gurov, D. (2009):
Provably Correct Runtime Monitoring.
Journal of Logic and Algebraic Programming 78: 304-339 [Details]
Aktug, I.; Dam, M.; Gurov, D. (2008):
Provably correct runtime monitoring (extended abstract).
[Conference paper] 15th International Symposium on Formal Methods Location: Turku, FINLAND Date: MAY 26-30, 2008; Fm 2008: Formal Methods, Proceedings 262-277 [Details]
Wuhib, F.; Dam, M.; Stadler, R. (2008):
Decentralized detection of global threshold crossings using aggregation trees.
Computer Networks 52: 1745-1761 [Details]
Cohen, M.; Dam, M. (2007):
A complete axiomatization of knowledge and cryptography.
[Conference paper] 22nd Annual IEEE Symposium on Logic in Computer Science Location: Wroclaw, Poland, Date: JUL 10-14, 2007; 22nd Annual IEEE Symposium On Logic In Computer Science, Proceedings 77-86 [Details]
Wuhib, F.; Dam, M.; Stadler, R.; Clemm, A. (2007):
Robust Monitoring of Network-wide Aggregates through Gossiping.
[Conference paper] 10th IFIP/IEEE International Symposium on Integrated Network Management Munich, GERMANY, MAY 21-25, 2007; IFIP/IEEE International Symposium on Integrated Network Management (IM 2009) 226-235 [Details]

More