Skip to main content

Publications by Mads Dam

Refereegranskade

Artiklar

[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.

Konferensbidrag

[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.

Kapitel i böcker

[56]
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

Artiklar

[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.

Kapitel i böcker

[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.

Rapporter

[60]
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