Publications by Mads Dam

Peer reviewed

Articles

[1]

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.

[2]

R. Guanciale et al., "Provably secure memory isolation for Linux on ARM," Journal of Computer Security, vol. 24, no. 6, pp. 793-837, 2016.

[3]

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.

[4]

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.

[5]

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.

[6]

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.

[7]

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.

[8]

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.

[9]

M. Dam, "Decidability and proof systems for language-based noninterference relations," SIGPLAN notices, vol. 41, no. 1, pp. 67-78, 2006.

[10]

M. Dam, "Regular SPKI," Lecture Notes in Computer Science, vol. 3364, pp. 134-152, 2005.

[11]

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.

[12]

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.

[13]

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.

Conference papers

[14]

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.

[15]

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.

[16]

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.

[17]

C. Baumann et al., "On Compositional Information Flow Aware Refinement," in 2021 IEEE 34Th Computer Security Foundations Symposium (CSF 2021), 2021, pp. 17-32.

[18]

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.

[19]

D. Lundberg et al., "Hoare-Style Logic for Unstructured Programs," in Software Engineering and Formal Methods, 2020, pp. 193-213.

[20]

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.

[21]

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.

[22]

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.

[23]

O. Schwarz and M. Dam, "Automatic Derivation of Platform Noninterference Properties," in Software Engineering and Formal Methods, Springer LNCS 9763, 2016, pp. 27-44.

[24]

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.

[25]

H. Nemati et al., "Trustworthy Memory Isolation of Linux on Embedded Devices," in Trust and Trustworthy Computing, TRUST 2015, 2015, pp. 125-142.

[26]

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.

[27]

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.

[28]

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.

[29]

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.

[30]

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.

[31]

K. Palmskog et al., "ABS-NET: Fully Decentralized Runtime Adaptation for Distributed Objects," in Proceedings 6th Interaction and Concurrency Experience, 2013, pp. 85-100.

[32]

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.

[33]

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.

[34]

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.

[35]

M. Dam, R. Guanciale and H. Nemati, "Machine Code Verification of a Tiny ARM Hypervisor," in TrustED 13, November 4 2013, Berlin, Germany, 2013.

[36]

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.

[37]

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.

[38]

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.

[39]

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.

[40]

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.

[41]

K. Palmskog et al., "Scalable Metadata-Directed Search in a Network of Information," in Future Network and MobileSummit 2010 Conference Proceedings, 2010, p. 5722376.

[42]

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.

[43]

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.

[44]

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.

[45]

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.

[46]

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.

[47]

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.

[48]

M. Dam et al., "Security Monitor Inlining for Multithreaded Java," in ECOOP 2009 : OBJECT-ORIENTED PROGRAMMING, 2009, pp. 546-569.

[49]

I. Aktug, M. Dam and D. Gurov, "Provably correct runtime monitoring (extended abstract)," in Fm 2008: Formal Methods, Proceedings, 2008, pp. 262-277.

[50]

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.

[51]

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.

[52]

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.

[53]

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.

[54]

M. Cohen and M. Dam, "Epistemic logic, Cryptography, Logical Omniscience, BAN Logic," in Methods for Modalities (M4M), 2005.

[55]

M. Cohen and M. Dam, "Logical Omniscience in the Semantics of BAN Logics," in Proc.FCS´05, 2005.

Chapters in books

[56]

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

Non-peer reviewed

Articles

[57]

M. Dam and K. Palmskog, "Location Independent Routing in Process Network Overlays," Service Oriented Computing and Applications, no. Special Issue, pp. 1-25, 2014.

[58]

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.

Chapters in books

[59]

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.