Publikationer av Mads Dam

Refereegranskade

Artiklar

[1]

C. Baumann, O. Schwarz och M. Dam, "On the verification of system-level information flow properties for virtualized execution platforms," Journal of Cryptographic Engineering, vol. 9, no. 3, s. 243-261, 2019.

[2]

R. Guanciale et al., "Provably secure memory isolation for Linux on ARM," Journal of Computer Security, vol. 24, no. 6, s. 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, s. 528-565, 2015.

[4]

D. Guelev och M. Dam, "An epistemic predicate CTL* for finite control pi-processes," Electronical Notes in Theoretical Computer Science, vol. 278, no. 1, s. 229-243, 2011.

[5]

F. Wuhib, M. Dam och R. Stadler, "A Gossiping Protocol for Detecting Global Threshold Crossings," IEEE Transactions on Network and Service Management, vol. 7, no. 1, s. 42-57, 2010.

[6]

I. Aktug, M. Dam och D. Gurov, "Provably Correct Runtime Monitoring," Journal of Logic and Algebraic Programming, vol. 78, no. 5, s. 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, s. 95-109, 2009.

[8]

F. Wuhib, M. Dam och R. Stadler, "Decentralized detection of global threshold crossings using aggregation trees," Computer Networks, vol. 52, no. 9, s. 1745-1761, 2008.

[9]

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

[10]

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

[11]

P. Giambiagi och M. Dam, "On the secure implementation of security protocols," Science of Computer Programming, vol. 50, no. 3-Jan, s. 73-99, 2004.

[12]

C. Sprenger och M. Dam, "On global induction mechanisms in a mu-calculus with explicit approximations," RARIO : Informatique théorique et applications, vol. 37, no. 4, s. 365-391, 2003.

[13]

M. Dam och D. Gurov, "mu-calculus with explicit points and approximations," Journal of logic and computation (Print), vol. 12, no. 2, s. 255-269, 2002.

Konferensbidrag

[14]

N. Dong et al., "Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor," i 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," i Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022, 2022, s. 129-138.

[16]

A. Alshnakat et al., "HOL4P4 : Semantics for a Verified Data Plane," i EuroP4 2022 : Proceedings of the 5th International Workshop on P4 in Europe, Part of CoNEXT 2022, 2022, s. 39-45.

[17]

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

[18]

N. Dong, R. Guanciale och M. Dam, "Refinement-Based Verification of Device-to-Device Information Flow," i 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," i Software Engineering and Formal Methods, 2020, s. 193-213.

[20]

R. Guanciale, M. Balliu och M. Dam, "InSpectre : Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis," i 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," 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, 2018, s. 109-133.

[22]

C. Baumann, O. Schwarz och M. Dam, "Compositional Verification of Security Properties for Embedded Execution Platforms," i PROOFS 2017 : 6th International Workshop on Security Proofs for Embedded Systems, 2017, s. 1-16.

[23]

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

[24]

R. Guanciale et al., "Cache Storage Channels : Alias-Driven Attacks and Verified Countermeasures," i Proceedings - 2016 IEEE Symposium on Security and Privacy, SP 2016, 2016, s. 38-55.

[25]

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

[26]

H. Chfouka et al., "Trustworthy prevention of code injection in Linux on embedded devices," i 20th European Symposium on Research in Computer Security, ESORICS 2015, 2015, s. 90-107.

[27]

H. Nemati, R. Guanciale och M. Dam, "Trustworthy virtualization of the ARMv7 memory subsystem," i 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015, 2015, s. 578-589.

[28]

M. Balliu, M. Dam och R. Guanciale, "Automating Information Flow Analysis of Low Level Code," i Proceedings of CCS’14, November 3–7, 2014, Scottsdale, Arizona, USA, 2014.

[29]

O. Schwarz och M. Dam, "Formal Verification of Secure User Mode Device Execution with DMA," i Hardware and Software : Verification and Testing, 2014, s. 236-251.

[30]

M. Dam och K. Palmskog, "Location independent routing in process network overlays," i Proceedings - 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014, 2014, s. 715-724.

[31]

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

[32]

M. Dam och K. Palmskog, "Efficient and fully abstract routing of futures in object network overlays," i AGERE! 2013 - Proceedings of the 2013 ACM Workshop on Programming Based on Actors, Agents, and Decentralized Control, 2013, s. 49-59.

[33]

M. Dam et al., "Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel," i 2013 ACM SIGSAC Conference on Computer & Communications Security (CCS'13),November 4 - 8, 2013 Berlin, Germany, 2013.

[34]

N. Khakpour, O. Schwarz och M. Dam, "Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties," i Certified Programs and Proofs : Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, 2013, s. 276-291.

[35]

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

[36]

M. Balliu, M. Dam och G. Le Guernic, "ENCOVER : Symbolic Exploration for Information Flow Security," i 2012 IEEE 25th Computer Security Foundations Symposium (CSF), 2012, s. 30-44.

[37]

G. Kreitz, M. Dam och D. Wikström, "Practical Private Information Aggregation in Large Networks," i Information Security Technology For Applications, 2012, s. 89-103.

[38]

M. Dam, G. Le Guernic och A. Lundblad, "TreeDroid : A tree automaton based approach to enforcing data processing policies," i CCS '12 Proceedings of the 2012 ACM conference on Computer and communications security, 2012, s. 894-905.

[39]

M. Balliu, M. Dam och G. Le Guernic, "Epistemic Temporal Logic for Information Flow Security," i 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," i PODC 2010 : PROCEEDINGS OF THE 2010 ACM SYMPOSIUM ON PRINCIPLES OF DISTRIBUTED COMPUTING, 2010, s. 291-292.

[41]

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

[42]

K. V. Jónsson och M. Dam, "Towards Flexible and Secure Distributed Aggregation," i MECHANISMS FOR AUTONOMOUS MANAGEMENT OF NETWORKS AND SERVICES, 2010, s. 159-162.

[43]

M. Cohen et al., "A data symmetry reduction technique for temporal-epistemic logic," i Automated Technology for Verification and Analysis : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, 2009, s. 69-83.

[44]

M. Cohen et al., "A symmetry reduction technique for model checking temporal epistemic logic," i 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, s. 721-726.

[45]

M. Cohen et al., "Abstraction in Model Checking Multi-agent Systems," i AAMAS '09 Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems, 2009, s. 710-717.

[46]

R. Stadler et al., "Decentralized real-time monitoring of network-wide aggregates," i Proceedings of the 2nd Workshop on Large-Scale Distributed Systems and Middleware, 2009.

[47]

F. Wuhib, R. Stadler och M. Dam, "Gossiping for Threshold Detection," i 2009 IFIP/IEEE INTERNATIONAL SYMPOSIUM ON INTEGRATED NETWORK MANAGEMENT (IM 2009) VOLS 1 AND 2, 2009, s. 259-266.

[48]

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

[49]

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

[50]

M. Cohen och M. Dam, "A complete axiomatization of knowledge and cryptography," i 22nd Annual IEEE Symposium On Logic In Computer Science, Proceedings, 2007, s. 77-86.

[51]

F. Z. Wuhib et al., "Robust Monitoring of Network-wide Aggregates through Gossiping," i IFIP/IEEE International Symposium on Integrated Network Management (IM 2009) : VOLS 1 AND 2, 2007, s. 226-235.

[52]

M. Dam och R. Stadler, "A Generic Protocol for Network State Aggregation," i 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," i IFIP/IEEE International Workshop on Distributed Systems : Operations and Management, 2005, s. 220-232.

[54]

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

[55]

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

Kapitel i böcker

[56]

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

Icke refereegranskade

Artiklar

[57]

M. Dam och K. Palmskog, "Location Independent Routing in Process Network Overlays," Service Oriented Computing and Applications, no. Special Issue, s. 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, s. 37-59, 2010.

Kapitel i böcker

[59]

R. Guanciale et al., "A Case Study in Information Flow Refinement for Low Level Systems," i The Logic of Software. A Tasting Menu of Formal Methods, : Springer Nature, 2022, s. 54-79.