Skip to main content

Publications by Mads Dam



C. Baumann, O. Schwarz and M. Dam, "On the verification of system-level information flow properties for virtualized execution platforms," Journal of Cryptographic Engineering, vol. 9, no. 3, pp. 243-261, 2019.
R. Guanciale et al., "Provably secure memory isolation for Linux on ARM," Journal of Computer Security, vol. 24, no. 6, pp. 793-837, 2016.
M. Dam et al., "Security monitor inlining and certification for multithreaded Java," Mathematical Structures in Computer Science, vol. 25, no. 3, pp. 528-565, 2015.
D. Guelev and M. Dam, "An epistemic predicate CTL* for finite control pi-processes," Electronical Notes in Theoretical Computer Science, vol. 278, no. 1, pp. 229-243, 2011.
F. Wuhib, M. Dam and R. Stadler, "A Gossiping Protocol for Detecting Global Threshold Crossings," IEEE Transactions on Network and Service Management, vol. 7, no. 1, pp. 42-57, 2010.
I. Aktug, M. Dam and D. Gurov, "Provably Correct Runtime Monitoring," Journal of Logic and Algebraic Programming, vol. 78, no. 5, pp. 304-339, 2009.
W. Fetahi et al., "Robust Monitoring of Network-wide Aggregates through Gossiping," IEEE Transactions on Network and Service Management, vol. 6, no. 2, pp. 95-109, 2009.
F. Wuhib, M. Dam and R. Stadler, "Decentralized detection of global threshold crossings using aggregation trees," Computer Networks, vol. 52, no. 9, pp. 1745-1761, 2008.
M. Dam, "Decidability and proof systems for language-based noninterference relations," SIGPLAN notices, vol. 41, no. 1, pp. 67-78, 2006.
M. Dam, "Regular SPKI," Lecture Notes in Computer Science, vol. 3364, pp. 134-152, 2005.
P. Giambiagi and M. Dam, "On the secure implementation of security protocols," Science of Computer Programming, vol. 50, no. 3-Jan, pp. 73-99, 2004.
C. Sprenger and M. Dam, "On global induction mechanisms in a mu-calculus with explicit approximations," RARIO : Informatique théorique et applications, vol. 37, no. 4, pp. 365-391, 2003.
M. Dam and D. Gurov, "mu-calculus with explicit points and approximations," Journal of logic and computation (Print), vol. 12, no. 2, pp. 255-269, 2002.


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.
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.
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.
C. Baumann et al., "On Compositional Information Flow Aware Refinement," in 2021 IEEE 34Th Computer Security Foundations Symposium (CSF 2021), 2021, pp. 17-32.
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.
D. Lundberg et al., "Hoare-Style Logic for Unstructured Programs," in Software Engineering and Formal Methods, 2020, pp. 193-213.
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.
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.
C. Baumann, O. Schwarz and M. Dam, "Compositional Verification of Security Properties for Embedded Execution Platforms," in PROOFS 2017 : 6th International Workshop on Security Proofs for Embedded Systems, 2017, pp. 1-16.
O. Schwarz and M. Dam, "Automatic Derivation of Platform Noninterference Properties," in Software Engineering and Formal Methods, Springer LNCS 9763, 2016, pp. 27-44.
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.
H. Nemati et al., "Trustworthy Memory Isolation of Linux on Embedded Devices," in Trust and Trustworthy Computing, TRUST 2015, 2015, pp. 125-142.
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.
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.
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.
O. Schwarz and M. Dam, "Formal Verification of Secure User Mode Device Execution with DMA," in Hardware and Software : Verification and Testing, 2014, pp. 236-251.
M. Dam and K. Palmskog, "Location independent routing in process network overlays," in Proceedings - 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014, 2014, pp. 715-724.
K. Palmskog et al., "ABS-NET: Fully Decentralized Runtime Adaptation for Distributed Objects," in Proceedings 6th Interaction and Concurrency Experience, 2013, pp. 85-100.
M. Dam and K. Palmskog, "Efficient and fully abstract routing of futures in object network overlays," in AGERE! 2013 - Proceedings of the 2013 ACM Workshop on Programming Based on Actors, Agents, and Decentralized Control, 2013, pp. 49-59.
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.
N. Khakpour, O. Schwarz and M. Dam, "Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties," in Certified Programs and Proofs : Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, 2013, pp. 276-291.
M. Dam, R. Guanciale and H. Nemati, "Machine Code Verification of a Tiny ARM Hypervisor," in TrustED 13, November 4 2013, Berlin, Germany, 2013.
M. Balliu, M. Dam and G. Le Guernic, "ENCOVER : Symbolic Exploration for Information Flow Security," in 2012 IEEE 25th Computer Security Foundations Symposium (CSF), 2012, pp. 30-44.
G. Kreitz, M. Dam and D. Wikström, "Practical Private Information Aggregation in Large Networks," in Information Security Technology For Applications, 2012, pp. 89-103.
M. Dam, G. Le Guernic and A. Lundblad, "TreeDroid : A tree automaton based approach to enforcing data processing policies," in CCS '12 Proceedings of the 2012 ACM conference on Computer and communications security, 2012, pp. 894-905.
M. Balliu, M. Dam and G. Le Guernic, "Epistemic Temporal Logic for Information Flow Security," in In proc. of th 4e ACM SIGPLAN workshop on Programming Languages and Analysis for Security, 2011.
S. Krishnamurthy et al., "Brief Announcement: The Accuracy of Tree-based Counting in Dynamic Networks," in PODC 2010 : PROCEEDINGS OF THE 2010 ACM SYMPOSIUM ON PRINCIPLES OF DISTRIBUTED COMPUTING, 2010, pp. 291-292.
K. Palmskog et al., "Scalable Metadata-Directed Search in a Network of Information," in Future Network and MobileSummit 2010 Conference Proceedings, 2010, p. 5722376.
K. V. Jónsson and M. Dam, "Towards Flexible and Secure Distributed Aggregation," in MECHANISMS FOR AUTONOMOUS MANAGEMENT OF NETWORKS AND SERVICES, 2010, pp. 159-162.
M. Cohen et al., "A data symmetry reduction technique for temporal-epistemic logic," in Automated Technology for Verification and Analysis : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, 2009, pp. 69-83.
M. Cohen et al., "A symmetry reduction technique for model checking temporal epistemic logic," in 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, pp. 721-726.
M. Cohen et al., "Abstraction in Model Checking Multi-agent Systems," in AAMAS '09 Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems, 2009, pp. 710-717.
R. Stadler et al., "Decentralized real-time monitoring of network-wide aggregates," in Proceedings of the 2nd Workshop on Large-Scale Distributed Systems and Middleware, 2009.
F. Wuhib, R. Stadler and M. Dam, "Gossiping for Threshold Detection," in 2009 IFIP/IEEE INTERNATIONAL SYMPOSIUM ON INTEGRATED NETWORK MANAGEMENT (IM 2009) VOLS 1 AND 2, 2009, pp. 259-266.
M. Dam et al., "Security Monitor Inlining for Multithreaded Java," in ECOOP 2009 : OBJECT-ORIENTED PROGRAMMING, 2009, pp. 546-569.
I. Aktug, M. Dam and D. Gurov, "Provably correct runtime monitoring (extended abstract)," in Fm 2008: Formal Methods, Proceedings, 2008, pp. 262-277.
M. Cohen and M. Dam, "A complete axiomatization of knowledge and cryptography," in 22nd Annual IEEE Symposium On Logic In Computer Science, Proceedings, 2007, pp. 77-86.
F. Z. Wuhib et al., "Robust Monitoring of Network-wide Aggregates through Gossiping," in IFIP/IEEE International Symposium on Integrated Network Management (IM 2009) : VOLS 1 AND 2, 2007, pp. 226-235.
M. Dam and R. Stadler, "A Generic Protocol for Network State Aggregation," in Radiovetenskap och Kommunikation, RVK05. Linköping, Sweden. 14 juni - 15 juni 2005, 2005.
F. Z. Wuhib et al., "Decentralized computation of threshold crossing alerts," in IFIP/IEEE International Workshop on Distributed Systems : Operations and Management, 2005, pp. 220-232.
M. Cohen and M. Dam, "Epistemic logic, Cryptography, Logical Omniscience, BAN Logic," in Methods for Modalities (M4M), 2005.
M. Cohen and M. Dam, "Logical Omniscience in the Semantics of BAN Logics," in Proc.FCS´05, 2005.

Kapitel i böcker

D. Raz et al., "In-Network Monitoring," in Algorithms for Next Generation Networks, Graham Cormode and Marina Thottan Ed., : Springer Publishing Company, 2010.

Icke refereegranskade


M. Dam and K. Palmskog, "Location Independent Routing in Process Network Overlays," Service Oriented Computing and Applications, no. Special Issue, pp. 1-25, 2014.
M. Dam et al., "Provably Correct Inline Monitoring for Multi-threaded Java-like Programs," Journal of Computer Security, vol. 18, no. 1, pp. 37-59, 2010.

Kapitel i böcker

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.


M. Costa et al., "A future view on the Nakano district," Stockholm : KTH Royal Institute of Technology, 2018.

Proceedings (redaktörskap)

Senaste synkning med DiVA:
2024-04-21 02:30:55