biblio.bib

% This file was created with JabRef 2.10.
% Encoding: UTF-8

@InProceedings{eslh:asiaccs23,
	author                   = {Tiziano Marinaro and Pablo Buiras and Andreas Lindner and Roberto Guanciale and Hamed Nemati},
	title                    = {Beyond Over-Protection: A Targeted Approach to Spectre Mitigation and Performance Optimization},
	booktitle                = {Proceedings of the 2024 ACM ASIA Conference on Computer and Communications Security (ACM ASIACCS)},
	year                     = {2024},
	url                      = {http://arxiv.org/abs/2312.09770},
	Abstract                 = {Since the advent of Spectre attacks, researchers and practitioners have developed a range of hardware and software measures to counter transient execution attacks. A prime example of such mitigation is speculative load hardening in LLVM, which protects against leaks by tracking the speculation state and masking values during misspeculation. LLVM relies on static analysis to harden programs using slh that often results in over-protection, which incurs performance overhead. We extended an existing side-channel model validation framework, Scam-V, to check the vulnerability of programs to Spectre-PHT attacks and optimize the protection of programs using the slh approach. We illustrate the efficacy of Scam-V by first demonstrating that it can automatically identify Spectre vulnerabilities in real programs, e.g., fragments of crypto-libraries. We then develop an optimization mechanism that validates the necessity of slh hardening w.r.t. the target platform. Our experiments showed that hardening introduced by LLVM in most cases could be significantly improved when the underlying microarchitecture properties are considered.}
}

@InProceedings{serberus:sp24,
	author                   = {Nicholas Mosier and Hamed Nemati and John Mitchell and Caroline Trippel},
	title                    = {Serberus: Protecting Cryptographic Code from Spectres at Compile-Time},
	booktitle                = {Proceedings of the 45th IEEE Symposium on Security and Privacy},
	year                     = {2024},
	url                      = {paper/mosier_SP24.pdf},
	Abstract                 = {We design and formally prove the completeness of Serberus, the first comprehensive mitigation for hardening constant-time (CT) code against Spectre attacks (involving the PHT, BTB, RSB, STL, and/or PSF speculation primitives) on existing hardware. Serberus is based on three insights. First, hardware control-flow integrity (CFI) protections restrict transient control-flow to the extent that it may be comprehensively considered by software analyses. Second, conformance to the accepted CT code discipline permits two code patterns that are unsafe in the post-Spectre era. Finally, once these code patterns are addressed, all Spectre leakage of secrets in CT programs can be attributed to one of four classes of taint primitives, instructions which can transiently assign a secret value to a publicly-typed variable. We empirically evaluate Serberus on cryptographic primitives in the OpenSSL, Libsodium, and HACL libraries. Serberus introduces 20.4 runtime overhead on average, compared to 24.9 for the next closest state-of-the-art software mitigation, which features weaker security guarantees.}
}

@InProceedings{kconcurrency,
	author                   = {Mads Dam and Hamed Nemati},
	title                    = {Compositional Verification Using Past-Time Epistemic Temporal Logic},
	booktitle                = {Non-refereed},
	year                     = {2024},
	url                      = {paper/ptetl.pdf},
	Abstract                 = {Reasoning about shared variable concurrent programs poses significant challenges due to the need to account for interference between concurrently executing threads. Traditional verification approaches often fall short in terms of modularity and composability, which are essential for scalable and maintainable verification. We present a method for modular and compositional verification of concurrent programs using \textit{past-time temporal epistemic logic}. Our approach builds on Halpern and Moses' epistemic logic framework and incorporates past-time temporal operators to capture the temporal context of thread interactions. We formalize the semantics of our logic, introduce a compositional proof system for reasoning about concurrent programs, and demonstrate its application using examples. The expressiveness of our proposed logic provides a rigorous foundation to verify concurrent systems compositionally.}
}

@InProceedings{cryptobap:ccs23,
	author                   = {Faezeh Nasrabadi and Robert K{\"u}nnemann and Hamed Nemati},
	title                    = {CryptoBap: A Binary Analysis Platform for Cryptographic Protocols},
	booktitle                = {Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security(CCS)},
	year                     = {2023},
	url                      = {paper/ccs2023b-paper320.pdf},
	Abstract                 = {We introduce CryptoBap, a platform to verify weak secrecy and authentication for the (ARMv8 and RISC-V) machine code of cryptographic protocols. We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution to automatically extract a model of the protocol that represents all its execution paths. Our symbolic execution resolves indirect jumps and supports bounded loops using the loop-summarization technique, which we fully automate. The extracted model is then translated into models amenable to automated verification via ProVerif and CryptoVerif using a third-party toolchain. We prove the soundness of the proposed approach and used CryptoBap to verify multiple case studies ranging from toy examples to real-world protocols, TinySSH, an implementation of SSH, and WireGaurd, a modern VPN protocol.}
}

@InProceedings{FetchBench:ccs23,
	author                   = {Till Schlüter and Amit Choudhari and Lorenz Hetterich and Leon Trampert and Hamed Nemati and Ahmad Ibrahim and Michael Schwarz and Christian Rossow and Nils Ole Tippenhauer},
	title                    = {FetchBench: Systematic Identification and Characterization of Proprietary Prefetchers},
	booktitle                = {Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security(CCS)},
	year                     = {2023},
	url                      = {paper/ccs23-fetchbench.pdf},	
	Abstract                 = {Prefetchers are features in modern CPUs that allow speculative fetching of memory based on predictions on future memory use of applications. Different CPU models may use different prefetcher types, and two implementations of the same prefetcher can differ in detail in their characteristics, leading to distinct runtime behavior. For a few implementations, security researchers showed through manual analysis how to exploit specific prefetchers to leak secret data. Identifying such vulnerabilities required tedious reverse-engineering as prefetcher implementations are proprietary and undocumented. So far, no systematic study of prefetchers in common CPUs is available, preventing further security assessment. In this work, we address the following question: How can we systematically identify and characterize under-specified prefetchers in proprietary processors? To answer this question, we systematically analyze approaches to prefetching, design cross-platform tests to identify and characterize them on a given CPU, and demonstrate that our implementation FetchBench can characterize prefetchers on 14 different ARM and x86-64 CPUs. For example, FetchBench uncovers and characterizes a previously unknown replay-based prefetcher on the ARM Cortex-A72 CPU. Based on these findings, we demonstrate two novel attacks that exploit this undocumented prefetcher as a side channel to leak secret information, even from the secure TrustZone into normal world.},
	Miscellaneous            = {<a class="fas fa-bug" aria-hidden="true" href='https://developer.arm.com/Arm%20Security%20Center/Prefetcher%20Side%20Channels' style='color:#e4077d'> CVE-2023-33936 </a>}
}

@InProceedings{hwswspectremitigation:plarch23,
	author                   = {Nicholas Mosier and Kate Eselius and John Mitchell and Hamed Nemati and Caroline Trippel},
	booktitle                = {Workshop on Programming Languages for Architecture},
	year                     = {2023},
	url                      = {paper/plarch23.pdf},
	title                    = {Hardware-Software Codesign for Mitigating Spectre},
	Abstract                 = {Spectre attacks exploit control- and data-flow (mis)prediction on modern processors to transiently leak program secrets. Comprehensively mitigating Spectre leakage is hard, and doing so while preserving the program’s performance is even harder: no existing Spectre mitigations are widely deployed due to their high overhead or high complexity. We claim that a comprehensive, efficient, and low-complexity mitigation for Spectre attacks requires engaging in software-compiler-hardware co-design. In our talk, we will pitch such a co-designed Spectre mitigation that will be widely deployable at a low cost in security-critical applications. As a first step towards this goal, we have developed Serberus, a comprehensive and proven-correct Spectre mitigation for constant-time code that targets existing hardware. We are currently exploring lightweight hardware support to improve Serberus’ performance in other application domains.}
}

@InProceedings{seal:sacmat23,
	author                   = {Hamed Rasifard and Rahul Gopinath and Michael Backes and Hamed Nemati},
	title                    = {SEAL: Capability-Based Access Control for Data-Analytic Scenarios},
	booktitle                = {Proceedings of the 28th ACM Symposium on Access Control Models and Technologies, SACMAT 2023, Trento, Italy, June 7-9, 2023},
	pages                    = {67--78},
	year                     = {2023},
	crossref                 = {DBLP:conf/sacmat/2023},
	url                      = {https://doi.org/10.1145/3589608.3593838},
	doi                      = {10.1145/3589608.3593838},
	biburl                   = {https://dblp.org/rec/conf/sacmat/RasifardG0N23.bib},
	Abstract                 = {Data science is the basis for various disciplines in the Big-Data era. Due to the high volume, velocity, and variety of big data, data owners often store their data in data servers. Past few years, many computation techniques have emerged to protect the security and privacy of such shared data while enabling analysis thereon. Hence, access-control systems must provide a fine-grained, multi-layer mechanism to protect data. However, the existing systems and frameworks fail to satisfy all these requirements and resolve the trust issue between data owners and analysts. In this paper, we propose SEAL as a framework to protect the security and privacy of shared data. SEAL enables computations on shared data while they remain under the complete control of data owners through pre-defined policies. Our framework employs the capability-object model to define flexible access policies. SEAL's access-control system supports delegating and revoking access privileges and other access-control customizations. In addition, SEAL can assign security labels to privacy-sensitive data and track them to enable data owners to define where and when a data analyst can access their data. We demonstrate the practicability of our approach by presenting a prototype implementation of SEAL. Furthermore, we display the flexibility of our framework by implementing multiple data-analytic scenarios, which cover different applications.}
}


@InProceedings{nemati:microleakagetemplate,
	Author                   = {Hamed Nemati and Ahmad Ibrahim and Till Sch{\"u}ter and Nils Ole Tippenhauer and Christian Rossow},
	Title                    = {Microarchitectural Leakage Templates and Their Application to Cache Based Side Channels},
	Booktitle                = {Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security(CCS)},  
	Year                     = {2022},
	doi                      = {10.1145/3548606.3560613},
	url                      = {paper/ccs22-leakagetemplates.pdf},
	Artifact                 = {https://github.com/scy-phy/plumber},
	Abstract                 = {The complexity of modern processor architectures has given rise to sophisticated interactions among their components. Such interactions may result in potential attack vectors in terms of side channels, possibly available to userland exploits to leak secret data. Exploitation and countering of such side channels requires a detailed understanding of the target component. However, such detailed information is commonly unpublished for many CPUs. In this paper, we introduce the concept of Leakage Templates to abstractly describe specific side channels and identify their occurrences in binary applications. We design and implement Plumber, a framework to derive the generic Leakage Templates from individual code sequences that are known to cause leakage (e.g., found by prior work). Plumber uses a combination of instruction fuzzing, instructions’ operand mutation and statistical analysis to explore undocumented behavior of microarchitectural optimizations and derive sufficient conditions on vulnerable code inputs that if hold can trigger a distinguishing behavior. Using Plumber we dentified novel leakage primitives based on Leakage Templates (for ARM Cortex-A53 and -A72 cores), in articular related to previction (a new premature cache eviction), and prefetching behavior. We show the utility of Leakage Templates by re-identifying a prefetcher-based vulnerability in OpenSSL 1.1.0g first reported by Shin et al.},
	Miscellaneous            = {<a class="fas fa-video" aria-hidden="true" href='https://dl.cispa.de/s/FrBRm8DwJHjix4e' style='color:#e4077d'> Video recording </a>}
}

@InProceedings{DBLP:conf/isca/Nicholas22,
	Author                   = {Nicholas Mosier and Hanna Lachnitt and Hamed Nemati and Caroline Trippel},
	Title                    = {Axiomatic Hardware-Software Contracts for Security},
	BookTitle                = {49th {ACM/IEEE} Annual International Symposium on Computer Architecture({ISCA})},
	Year                     = {2022},
	Url                      = {paper/lcms_ISCA22_cameraready.pdf},
	Abstract                 = {We propose leakage containment models (LCMs)- novel axiomatic security contracts which support formally reasoning about the security guarantees of programs when they run on particular microarchitectures. Our core contribution is an axiomatic vocabulary for formally defining LCMs, derived from the established axiomatic vocabulary used to formalize processor memory consistency models. Using this vocabulary, we formalize microarchitectural leakage—focusing on leakage through hardware memory systems—so that it can be automatically detected in programs. To illustrate the efficacy of LCMs, we first demonstrate that our leakage definition faithfully captures a sampling of (transient and non-transient) microarchitectural attacks from the literature. Second, we develop a static analysis tool based on LCMs which automatically identifies Spectre vulnerabilities in programs and scales to analyze real-world crypto-libraries.},
	Artifact                 = {https://github.com/nmosier/clou},
        Miscellaneous            = {<a class="fas fa-blog" aria-hidden="true" href='https://www.openssl.org/blog/blog/2022/05/13/spectre-meltdown/' style='color:#e4077d'> OpenSSL OTC blog post </a>}
}  

@InProceedings{comprefinement22,
	Author                   = {Guanciale, Roberto and Baumann, Christoph and Buiras, Pablo and Dam, Mads and Nemati, Hamed},
	Title                    = {A Case Study in Information Flow Refinement for Low Level Systems},
	Booktitle                = {The Logic of Software. A Tasting Menu of Formal Methods},
	Year                     = {2022},
	doi                      = {10.1007/978-3-031-08166-8_4},
	Isbn                     = {978-3-031-08166-8},
	Pages                    = {54--79},
	Publisher                = {Springer International Publishing},
	Url                      = {paper/InfoFlowRefinementcasestudy.pdf},	
	Abstract                 = {In this work we employ information-flow-aware refinement to study security properties of a separation kernel. We focus on refinements that support changes in data representation and semantics, including the addition of state variables that may induce new observational power or side channels. We leverage an epistemic approach to ignorance-preserving refinement where an abstract model is used as a specification of a system's permitted information flows that may include the declassification of secret information. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. In particular, we show that a simple key manager may cause information leakage via a refinement that includes cache and timing information. Finally, we show that deploying standard countermeasures against cache-based timing channels regains ignorance preservation.}
}

@InProceedings{micro21,
	Month                    = {October},
	Author                   = {Hamed Nemati and Pablo Buiras and Andreas Lindner and Roberto Guanciale},
	Journal                  = {IEEE/ACM International Symposium on Microarchitecture},
	Title                    = {Validation of Side-Channel Models via Observation Refinement},
	BookTitle                = {2021 54th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO)},
	Year                     = {2021},
	Url                      = {paper/micro21.pdf},
	Abstract                 = {Observational models enable the analysis of information flow properties against side channels. Relational testing has been used to validate the soundness of these models by measuring the side channel on states that the model considers indistinguishable. However, unguided search can generate test states that are too similar to each other to invalidate the model. To address this we introduce observation refinement, a technique to guide the exploration of the state space to focus on hardware features of interest. We refine observational models to include fine-grained observations that characterize behavior that we want to exclude. States that yield equivalent refined observations are then ruled out, reducing the size of the space.},
        Artifact                 = {https://figshare.com/articles/software/Scam-V_MICRO_2021_artifact/15086895/3}
}

@InProceedings{usenix21,
	Month                    = {August},
	Author                   = {Daniel Weber and Ahmad Ibrahim and Hamed Nemati and Michael Schwarz and Christian Rossow},
	Journal                  = {USENIX Security Symposium},
	Title                    = {Osiris: Automated Discovery of Microarchitectural Side Channels},
	BookTitle                = {USENIX Security Symposium},
	Year                     = {2021},
	Url                      = {https://publications.cispa.saarland/3431/1/main.pdf},
	Abstract                 = {In the last Years, a plurality of side channels has been discovered on CPUs. These side channels have been used in powerful attacks, e.g., on cryptographic implementations, or as building blocks in transient-execution attacks such as Spectre or Meltdown. However, in many cases, discovering side channels is still a tedious manual process. In this paper, we present Osiris, a fuzzing-based framework to automatically discover microarchitectural side channels. Based on a machine-readable specification of a CPU's ISA, Osiris generates instruction-sequence triples and automatically tests whether they form a timing-based covert channel. Furthermore, Osiris evaluates their usability as a covert channel in transient-execution attacks, i.e., as the microarchitectural encoding for attacks like Spectre. In total, we discover four novel timing-based side channels on Intel and AMD CPUs. Based on these side channels, we demonstrate exploitation in three case studies. We show that our microarchitectural KASLR break using non-temporal loads, FlushConflict, is currently the only one that works on the new Intel Ice Lake and Comet Lake microarchitectures. We present a cross-core cross-VM covert channel that is not relying on the memory subsystem and transmits up to 1 kbit/s. We demonstrate this channel on the AWS cloud, showing that it is stealthy and noise resistant. Finally, we demonstrate Stream+Reload, a covert channel for transient-execution attacks that, on average, allows leaking 7.83 bytes within a transient window, improving state-of-the-art attacks that only leak up to 3 bytes.},
        Artifact                 = {https://github.com/cispa/osiris},
        Award                    = {CSAW'21 3rd place}        	
}

@InProceedings{icse3208,
	Month                    = {September},
	Author                   = {Rahul Gopinath and Hamed Nemati and Andreas Zeller},
	Journal                  = {International Conference on Software Engineering (ICSE)},
	Title                    = {Input Algebras},
	BookTitle                = {International Conference on Software Engineering (ICSE)},
	Year                     = {2021},
	Url                      = {https://publications.cispa.saarland/3208/},
	Abstract                 = {Grammar-based test generators are highly efficient in producing syntactically valid test inputs, and give their user precise control over which test inputs should be generated. Adapting a grammar or a test generator towards a particular testing goal can be tedious, though. We introduce the concept of a grammar transformer, specializing a grammar towards inclusion or exclusion of specific patterns: "The phone number must not start with 011 or +1". To the best of our knowledge, ours is the first approach to allow for arbitrary Boolean combinations of patterns, giving testers unprecedented flexibility in creating targeted software tests. The resulting specialized grammars can be used with any grammar-based fuzzer for targeted test generation, but also as validators to check whether the given specialization is met or not, opening up additional usage scenarios. In our evaluation on real-world bugs, we show that specialized grammars are accurate both in producing and validating targeted inputs.},
	Artifact                 = {https://nbviewer.org/github/vrthra/Ewoks/blob/master/src/FAlgebra.ipynb}
}

@InProceedings{KBRef2021,
	Title                    = {On Compositional Information Flow Aware Refinement},
	Author                   = {Christoph Baumann and Mads Dam and Roberto Guanciale and Hamed Nemati},
	BookTitle                = {IEEE Computer Security Foundations Symposium (CSF)},
	Year                     = {2021},
	Url                      = {paper/InfoFlowRefinement.pdf},
	Abstract                 = {The concepts of information flow security and refinement are known to have had a troubled relationship ever since the seminal work of McLean. In this work we study refinements that support changes in data representation and semantics, including the addition of state variables that may induce new observational power or side channels. We propose a new epistemic approach to ignorance-preserving refinement where an abstract model is used as a specification of a system’s permitted information flows, that may include the declassification of secret information. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. Our study is set in the context of a class of shared variable multi-agent models similar to interpreted systems in epistemic logic. We demonstrate the expressiveness of our framework through a series of small examples and compare our approach to existing, stricter notions of information-flow secure refinement based on bisimulations and noninterference preservation. Interestingly, noninterference preservation is not supported “out of the box” in our setting, because refinement steps may introduce new secrets that are independent of secrets already present at abstract level. To support verification, we first introduce a “cube-shaped” unwinding condition related to conditions recently studied in the context of value-dependent noninterference, kernel verification, and secure compilation. A fundamental problem with ignorance-preserving refinement, caused by the support for general data and observation refinement, is that sequential composability is lost. We propose a solution based on relational pre- and post-conditions and illustrate its use together with unwinding on the oblivious RAM construction of Chung and Pass.}  
}

@misc{nemati2020speculative,
	Title                    = {Speculative Leakage in ARM Cortex-A53 (short paper)},
	Author                   = {Hamed Nemati and Roberto Guanciale and Pablo Buiras and Andreas Lindner},
	Year                     = {2020},
	eprint                   ={2007.06865},
	Url                      = {https://arxiv.org/abs/2007.06865},
	archivePrefix            = {arXiv},
	primaryClass             = {cs.CR},
	Abstract = {The recent Spectre attacks have demonstrated that modern microarchitectural optimizations can make software insecure. These attacks use features like pipelining, out-of-order and speculation to extract information about the memory contents of a process via side-channels. In this paper we demonstrate that Cortex-A53 is affected by speculative leakage even if the microarchitecture does not support out-of-order execution. We named this new class of vulnerabilities SiSCloak.},
}

@InProceedings{SCAM-V20,
	Title                    = {Validation of abstract Side-channel Models for Computer Architectures},
	Author                   = {Hamed Nemati and Pablo Buiras and Andreas Lindner and Roberto Guanciale and Swen Jacobs},
	BookTitle                = {International Conference on Computer-Aided Verification (CAV)},
	Year                     = {2020},
	Url                      = {paper/scamv.pdf},
	Abstract                 = {Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs which invalidate the models due to hidden microarchitectural behavior.},
	Artifact                 = {https://github.com/kth-step/HolBA/tree/dev_scamv}	
}

@InProceedings{mitb19,
	Title                    = {MAC-in-the-Box: Verifying the Security of a Minimalistic Hardware Design for MAC Computation},
	Author                   = {Robert K{\"u}nnemann and Hamed Nemati},
	BookTitle                = {European Symposium on Research in Computer Security (ESORICS)},
	Year                     = {2020},
	Url                      = {paper/mitb-full.pdf},
	Abstract                 = {In this work, we study the verification of security properties of a minimalistic hardware design called the MAC-in-the-Box. This device computes a message authentication code based on the SHA-3 hash function and a key that is stored on device, but never output directly. It is designed for secure password storage, but may also be used for secure key-exchange and second-factor authentication. We formally verify that no outside observer can distinguish this device from an ideal functionality that provides only access to a hashing oracle.},
	Artifact                 = {https://github.com/rkunnema/mitb}
}

@inproceedings{DBLP:conf/tap/KhosrowjerdiNM20,
	Author                   = {Hojat Khosrowjerdi and Hamed Nemati and Karl Meinke},
	Title                    = {Spatio-Temporal Model-Checking of Cyber-Physical Systems Using Graph Queries},
	BookTitle                = {Tests and Proofs - 14th International Conference, TAP@STAF 2020, Bergen, Norway, June 22-23, 2020, Proceedings [postponed]},
	pages                    = {59--79},
	Year                     = {2020},
	crossref                 = {DBLP:conf/tap/2020},
	Url                      = {https://link.springer.com/chapter/10.1007/978-3-030-50995-8_4},
	doi                      = {10.1007/978-3-030-50995-8\_4},
	timestamp                = {Tue, 23 Jun 2020 17:11:48 +0200},
	bibUrl                   = {https://dblp.org/rec/conf/tap/KhosrowjerdiNM20.bib},
	bibsource                = {dblp computer science bibliography, https://dblp.org},
	Abstract                 = {We explore the application of graph database technology to spatio-temporal model checking of cooperating cyber-physical systems-of-systems such as vehicle platoons. We present a translation of spatio-temporal automata (STA) and the spatio-temporal logic STAL to semantically equivalent property graphs and graph queries respectively. We prove a sound reduction of the spatio-temporal verification problem to graph database query solving. The practicability and efficiency of this approach is evaluated by introducing NeoMC, a prototype implementation of our explicit model checking approach based on Neo4j. To evaluate NeoMC we consider case studies of verifying vehicle platooning models. Our evaluation demonstrates the effectiveness of our approach in terms of execution time and counterexample detection.}
}

@InProceedings{SCAM-V19,
	Title                    = {Validation of abstract Side-channel Models for Computer Architectures (short paper)},
	Author                   = {Andreas Lindner and Hamed Nemati and Pablo Buiras and Roberto Guanciale and Swen Jacobs},
	BookTitle                = {Online proceeding of ENTROPY Workshop 2019@EuroS&P},
	Year                     = {2019},
	Abstract                 = {Modern computer architectures include complex features that make it infeasible to analyze their effects on channels that may compromise program security. abstract side channel models have been proposed to approximate these flows in terms of system state observations, thus making the analysis tractable. However, using these models to verify security properties relies on the assumption that states with equivalent observations would be indistinguishable to the attacker on real hardware. In this work, we introduce a methodology and tool to validate side-channel models, testing program inputs that lead to equivalent observations in automatically-generated programs, and measuring against channels on the hardware. We partition the input state space based on the observation model and rely on an adaptive refinement of the model to guide the validation.}
}

@InProceedings{confllvm19,
	Author                   = {Ajay Brahmakshatriya and Piyus Kedia and Derrick P. McKee and Deepak Garg and Akash Lal and Aseem Rastogi and Hamed Nemati and Anmol Panda and Pratik Bhatu},
	Title                    = {ConfLLVM: A Compiler for Enforcing Data Confidentiality in Low-Level Code},
	Year                     = {2019},
	isbn                     = {9781450362818},
	publisher                = {Association for Computing Machinery},
	address                  = {New York, NY, USA},
	Url                      = {https://doi.org/10.1145/3302424.3303952},
	doi                      = {10.1145/3302424.3303952},
	BookTitle                = {Proceedings of the Fourteenth EuroSys Conference 2019},
	articleno                = {4},
	numpages                 = {15},
	location                 = {Dresden, Germany},
	series                   = {EuroSys'19},
	Abstract                 = {We present a compiler-based scheme for protecting the confidentiality of sensitive data in low-level applications (e.g. those written in C) in the presence of an active adversary. In  our scheme, the programmer marks sensitive data by writing lightweight annotations on the top-level definitions in the source code. The compiler then uses a combination of static dataflow analysis and runtime instrumentation to prevent data leaks even in the presence of low-level attacks. To reduce runtime overheads, the compiler uses a novel memory layout and a taint-aware form of control flow integrity. We formalize our scheme and prove its security. We have also implemented our scheme within the LLVM compiler and  evaluated it on the CPU-intensive SPEC micro-benchmarks, and on larger, real-world applications, including the NGINX webserver and the OpenLDAP directory server. We find that performance overheads introduced by our instrumentation are moderate (average 12% on SPEC), and the programmer effort to port the applications is minimal.}  
}

@InProceedings{CPRef2019,
	Title                    = {Confidentiality-Preserving Refinement},
	Author                   = {Roberto Guanciale and Christoph Baumann and Mads Dam and Hamed Nemati},
	BookTitle                = {PriSC},
	Year                     = {2019},
	Url                      = {https://popl19.sigplan.org/track/prisc-2019},
	Abstract                 = {We have developed a new formal framework to securely compile abstract specification (e.g. source language) to a refined model (e.g. assembly). Our goal is to prevent unintended leakage of secret data thus preserving the information flow of the abstract model, when they are transformed to a more refined system. The key idea of our approach is to use the abstract model as a specification of the permitted information flow, and then to ensure that this flow induces an upper bound on the corresponding flow in the refined model.},
}

@InProceedings{DBLP:conf/post/NematiBGD18,
	  Title                    = {Formal Verification of Integrity-Preserving Countermeasures Against
	 Cache Storage Side-Channels},
	  Author                   = {Hamed Nemati and Christoph Baumann and Roberto Guanciale and Mads Dam},
	  BookTitle                = {Principles of Security and Trust - 7th International Conference, {POST}
	 2018, Held as Part of the European Joint Conferences on Theory and
	 Practice of Software, {ETAPS} 2018, Thessaloniki, Greece, April 14-20,
	 2018, Proceedings},
	  Year                     = {2018},
	  Pages                    = {109--133},
	 
	  Bibsource                = {dblp computer science bibliography, https://dblp.org},
	  BibUrl                   = {https://dblp.org/rec/bib/conf/post/NematiBGD18},
	  Crossref                 = {DBLP:conf/post/2018},
	  Doi                      = {10.1007/978-3-319-89722-6_5},
	  Timestamp                = {Mon, 16 Apr 2018 13:28:26 +0200},
	  Url                      = {https://doi.org/10.1007/978-3-319-89722-6_5},
	  Abstract                 = {Formal verification of systems-level software such as hypervisors and operating systems can enhance system trustworthiness. However, without taking low level features like caches into account the verification may become unsound. While this is a well-known fact w.r.t. timing leaks, few works have addressed latent cache storage side-channels, whose effects are not limited to information leakage. We present a verification methodology to analyse soundness of countermeasures used to neutralise these channels. We apply the proposed methodology to existing countermeasures, showing that they allow to restore integrity of the system. We decompose the proof effort into verification conditions that allow for an easy adaption of our strategy to various software and hardware platforms. As case study, we extend the verification of an existing hypervisor whose integrity can be tampered using cache storage channels. We used the HOL4 theorem prover to validate our security analysis, applying the verification methodology to a generic hardware model.},
	  Artifact                 = {https://github.com/rauhbein/cacheproofs}  
}

@PhdThesis{DBLP:phd/basesearch/Nemati17,
	Title                    = {Secure System Virtualization: End-to-End Verification of Memory Isolation},
	Author                   = {Hamed Nemati},
	School                   = {Royal Institute of Technology, Stockholm, Sweden},
	Year                     = {2017},
	
	Bibsource                = {dblp computer science bibliography, https://dblp.org},
	BibUrl                   = {https://dblp.org/rec/bib/phd/basesearch/Nemati17},
	Timestamp                = {Fri, 20 Oct 2017 01:00:00 +0200},
	Url                      = {http://kth.diva-portal.org/smash/get/diva2:1136624/FULLTEXT03.pdf},
	Urn                      = {urn:nbn:se:kth:diva-213030},
	Abstract                 = {Over the last Years, security kernels have played a promising role in reshaping the landscape of platform security on today’s ubiquitous embedded devices. Security kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms. They reduce the software portion of the system’s trusted computing base to a thin layer, which enforces isolation between low- and high-criticality components. The reduced  trusted computing base minimizes the system attack surface and facilitates the use of formal methods to ensure functional correctness and security of the kernel. In this thesis, we explore various aspects of building a provably secure separation kernel using virtualization technology. In particular, we examine techniques related to the appropriate management of the memory subsystem. Once these techniques were implemented and functionally verified, they provide reliable a foundation for application scenarios that require strong guarantees of isolation and facilitate formal reasoning about the system’s overall security.}
}

@TechReport{Nemati1137182,
    Author                   = {Nemati, Hamed and Guanciale, Roberto and Baumann, Christoph and Dam, Mads},
    institution              = {KTH, Theoretical Computer Science, TCS},
    note                     = {QC 20170830},
    Title                    = {Formal Analysis of Countermeasures against Cache Storage Side Channels (technical report)},
    Url                      = {paper/FormalAnalysisofCountermeasures.pdf},
    Year                     = {2017},
    Abstract                 = {Formal verification of systems-level software such as hypervisors and operating systems can enhance system trustworthiness. However, without taking low level features like caches into account the verification may become unsound. While this is a well-known fact wrt. timing leaks, few works have addressed latent cache storage side-channels. We present a verification methodology to analyse soundness of countermeasures used to neutralise cache storage channels. We apply the proposed methodology to existing countermeasures, showing that they allow to restore integrity and prove confidentiality of the system. We decompose the proof effort into verification conditions that allow for an easy adaption of our strategy to various software and hardware platforms. As case study, we extend the verification of an existing hypervisor whose integrity can be tampered using cache storage channels. We used the HOL4 theorem prover to validate our security analysis, applying the verification methodology to formal models of ARMv7 and ARMv8}
}

@InProceedings{DBLP:conf/sp/GuancialeNBD16,
	Title                    = {Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures},
	Author                   = {Roberto Guanciale and Hamed Nemati and Christoph Baumann and Mads Dam},
	BookTitle                = {{IEEE} Symposium on Security and Privacy, {SP} 2016, San Jose, CA, USA, May 22-26, 2016},
	Year                     = {2016},
	Pages                    = {38--55},
	Bibsource                = {dblp computer science bibliography, https://dblp.org},
	BibUrl                   = {https://dblp.org/rec/bib/conf/sp/GuancialeNBD16},
	Crossref                 = {DBLP:conf/sp/2016},
	Doi                      = {10.1109/SP.2016.11},
	Timestamp                = {Fri, 26 May 2017 01:00:00 +0200},
	Url                      = {https://doi.org/10.1109/SP.2016.11},
	Abstract                 = {Caches pose a significant challenge to formal proofs of security for code executing on application processors, as the cache access pattern of security-critical services may leak secret information. This paper reveals a novel attack vector, exposing a low-noise cache storage channel that can be exploited by adapting well-known timing channel analysis techniques. The vector can also be used to attack various types of security-critical software such as hypervisors and application security monitors. The attack vector uses virtual aliases with mismatched memory attributes and self-modifying code to misconfigure the memory system, allowing an attacker to place incoherent copies of the same physical address into the caches and observe which addresses are stored in different levels of cache. We design and implement three different attacks using the new vector on trusted services and report on the discovery of an 128-bit key from an AES encryption service running in TrustZone on Raspberry Pi2. Moreover, we subvert the integrity properties of an ARMv7 hypervisor that was formally verified against a cache-less model. We evaluate well-known countermeasures against the new attack vector and propose a verification methodology that allows to formally prove the effectiveness of defence mechanisms on the binary code of the trusted software.}
}

@Article{DBLP:Journals/jcs/GuancialeNDB16,
	Title                    = {Provably secure memory isolation for Linux on {ARM}},
	Author                   = {Roberto Guanciale and Hamed Nemati and Mads Dam and Christoph Baumann},
	Journal                  = {Journal of Computer Security},
	Year                     = {2016},
	Number                   = {6},
	Pages                    = {793--837},
	Volume                   = {24},
	
	Bibsource                = {dblp computer science bibliography, https://dblp.org},
	BibUrl                   = {https://dblp.org/rec/bib/Journals/jcs/GuancialeNDB16},
	Doi                      = {10.3233/JCS-160558},
	Timestamp                = {Fri, 26 May 2017 01:00:00 +0200},
	Url                      = {https://doi.org/10.3233/JCS-160558},
	Abstract                 = {The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation and verification of a memory virtualization platform for ARMv7-A processors. The design is based on direct paging, an MMU virtualization mechanism previously introduced by Xen. It is shown that this mechanism can be implemented using a compact design, suitable for formal verification down to a low level of abstraction, without penalizing system performance. The verification is performed using the HOL4 theorem prover and uses a detailed model of the processor. We prove memory isolation along with information flow security for an abstract top-level model of the virtualization mechanism. The abstract model is refined down to a transition system closely resembling a C implementation. Additionally, it is demonstrated how the gap between the low-level abstraction and the binary level-can be filled, using tools that check Hoare contracts. The virtualization mechanism is demonstrated on real hardware via a hypervisor hosting Linux and supporting a tamper-proof run-time monitor that provably prevents code injection in the Linux guest.},
	Artifact                = {https://bitbucket.org/sicssec/sth/src/master/}  
}

@InProceedings{DBLP:conf/esorics/ChfoukaNGDE15,
	Title                    = {Trustworthy Prevention of Code Injection in Linux on Embedded Devices},
	Author                   = {Hind Chfouka and Hamed Nemati and Roberto Guanciale and Mads Dam and Patrik Ekdahl},
	BookTitle                = {Computer Security - {ESORICS} 2015 - 20th European Symposium on Research in Computer Security, Vienna, Austria, September 21-25, 2015, Proceedings, Part {I}},
	Year                     = {2015},
	Pages                    = {90--107},
	
	Bibsource                = {dblp computer science bibliography, https://dblp.org},
	BibUrl                   = {https://dblp.org/rec/bib/conf/esorics/ChfoukaNGDE15},
	Crossref                 = {DBLP:conf/esorics/2015-1},
	Doi                      = {10.1007/978-3-319-24174-6_5},
	Timestamp                = {Tue, 23 May 2017 01:07:16 +0200},
	Url                      = {https://doi.org/10.1007/978-3-319-24174-6_5},
	Abstract                 = {We present MProsper, a trustworthy system to prevent code injection in Linux on embedded devices. MProsper is a formally verified run-time monitor, which forces an untrusted Linux to obey the executable space protection policy; a memory area can be either executable or writable, but cannot be both. The executable space protection allows the MProsper’s monitor to intercept every change to the executable code performed by a user application or by the Linux kernel. On top of this infrastructure, we use standard code signing to prevent code injection. MProsper is deployed on top of the Prosper hypervisor and is implemented as an isolated guest. Thus MProsper inherits the security property verified for the hypervisor: (i) Its code and data cannot be tampered by the untrusted Linux guest and (ii) all changes to the memory layout is intercepted, thus enabling MProsper to completely mediate every operation that can violate the desired security property. The verification of the monitor has been performed using the HOL4 theorem prover and by extending the existing formal model of the hypervisor with the formal specification of the high level model of the monitor.}
}

@InProceedings{DBLP:conf/trust/NematiDGDV15,
	Title                    = {Trustworthy Memory Isolation of Linux on Embedded Devices},
	Author                   = {Hamed Nemati and Mads Dam and Roberto Guanciale and Viktor Do and Arash Vahidi},
	BookTitle                = {Trust and Trustworthy Computing - 8th International Conference, {TRUST} 2015, Heraklion, Greece, August 24-26, 2015, Proceedings},
	Year                     = {2015},
	Pages                    = {125--142},
	
	Bibsource                = {dblp computer science bibliography, https://dblp.org},
	BibUrl                   = {https://dblp.org/rec/bib/conf/trust/NematiDGDV15},
	Crossref                 = {DBLP:conf/trust/2015},
	Doi                      = {10.1007/978-3-319-22846-4_8},
	Timestamp                = {Tue, 23 May 2017 01:08:12 +0200},
	Url                      = {https://doi.org/10.1007/978-3-319-22846-4_8},
	Abstract                 = {The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself, for instance by run-time monitoring. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation and verification of a virtualization platform for the ARMv7-A processor family. Our design is based on direct paging, an MMU virtualization mechanism previously introduced by Xen for the x86 architecture, and used later with minor variants by the Secure Virtual Architecture, SVA. We show that the direct paging mechanism can be implemented using a compact design, suitable for formal verification down to a low level of abstraction, without penalizing system performance. The verification is performed using the HOL4 theorem prover and uses a detailed model of the ARMv7-A ISA, including the MMU. We prove memory isolation of the hosted components along with information flow security for an abstract top level model of the virtualization mechanism. The abstract model is refined down to a HOL4 transition system closely resembling a C implementation. The virtualization mechanism is demonstrated on real hardware via a hypervisor capable of hosting Linux as an untrusted guest.}
}

@InProceedings{DBLP:conf/sofsem/NematiGD15,
	Title                    = {Trustworthy Virtualization of the ARMv7 Memory Subsystem},
	Author                   = {Hamed Nemati and Roberto Guanciale and Mads Dam},
	BookTitle                = {{SOFSEM} 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science,  Pec pod Sn{\v{e}}{\v{z}}kou, Czech Republic, January 24-29, 2015. Proceedings},
	Year                     = {2015},
	Pages                    = {578--589},
	
	Bibsource                = {dblp computer science bibliography, https://dblp.org},
	BibUrl                   = {https://dblp.org/rec/bib/conf/sofsem/NematiGD15},
	Crossref                 = {DBLP:conf/sofsem/2015},
	Doi                      = {10.1007/978-3-662-46078-8_48},
	Timestamp                = {Thu, 15 Jun 2017 21:37:45 +0200},
	Url                      = {https://doi.org/10.1007/978-3-662-46078-8_48},
	Abstract                 = {In order to host a general purpose operating system, hypervisors need to virtualize the CPU memory subsystem. This entails dynamically changing MMU resources, in particular the page tables, to allow a hosted OS to recongure its own memory. In this paper we present the verication of the isolation properties of a hypervisor design that uses direct paging. This virtualization approach allows to host commodity OSs without requiring either shadow data structures or specialized hardware support. Our verication targets a system consisting of a commodity guest running Linux.The verication involves three steps: (i) Formalization of an ARMv7 CPU that includes the MMU, (ii) Formalization of a system behavior that includes the hypervisor and the untrusted guest (iii) Verication of the isolation properties. Formalization and proof are done in the HOL4 theorem prover, thus allowing to re-use the existing HOL4 ARMv7 model developed in Cambridge.}
}

@InProceedings{DBLP:conf/ccs/DamGKNS13,
	Title                    = {Formal verification of information flow security for a simple arm-based separation kernel},
	Author                   = {Mads Dam and Roberto Guanciale and Narges Khakpour and Hamed Nemati and Oliver Schwarz},
	BookTitle                = {2013 {ACM} {SIGSAC} Conference on Computer and Communications Security, CCS'13, Berlin, Germany, November 4-8, 2013},
	Year                     = {2013},
	Pages                    = {223--234},
	
	Bibsource                = {dblp computer science bibliography, https://dblp.org},
	BibUrl                   = {https://dblp.org/rec/bib/conf/ccs/DamGKNS13},
	Crossref                 = {DBLP:conf/ccs/2013},
	Doi                      = {10.1145/2508859.2516702},
	Timestamp                = {Fri, 08 Nov 2013 09:43:20 +0100},
	Url                      = {http://doi.acm.org/10.1145/2508859.2516702},
	Abstract                 = {A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information flow security for a simple separation kernel for ARMv7. Previous work on information flow kernel security leaves communication to be handled by model-external means, and cannot be used to draw conclusions when there is explicit interaction between partitions. We propose a different approach where communication between partitions is made explicit and the information flow is analyzed in the presence of such a channel. Limiting the kernel functionality as much as meaningfully possible, we accomplish a detailed analysis and verification of the system, proving its correctness at the level of the ARMv7 assembly. As a sanity check we show how the security condition is reduced to noninterference in the special case where no communication takes place. The verification is done in HOL4 taking the Cambridge model of ARM as basis, transferring verification tasks on the actual assembly code to an adaptation of the BAP binary analysis tool developed at CMU.},
	  Bibsource                = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/ccs/DamGN13,
	Title                    = {Machine code verification of a tiny {ARM} hypervisor},
	Author                   = {Mads Dam and Roberto Guanciale and Hamed Nemati},
	BookTitle                = {TrustED'13, Proceedings of the 2013 {ACM} Workshop on Trustworthy Embedded Devices, Co-located with {CCS} 2013, November 4, 2013, Berlin,  Germany},
	Year                     = {2013},
	Pages                    = {3--12},
	
	Bibsource                = {dblp computer science bibliography, https://dblp.org},
	BibUrl                   = {https://dblp.org/rec/bib/conf/ccs/DamGN13},
	Crossref                 = {DBLP:conf/ccs/2013trusted},
	Doi                      = {10.1145/2517300.2517302},
	Timestamp                = {Fri, 31 Jan 2014 10:38:00 +0100},
	Url                      = {http://doi.acm.org/10.1145/2517300.2517302},
	Abstract                 = {Hypervisors are low level execution platforms that provide isolated partitions on shared resources, allowing to design secure systems without using dedicated hardware devices. A key requirement of this kind of solution is the formal verification of the software trusted computing base, preferably at the binary level. We accomplish a detailed verification of an ARMv7 tiny hypervisor, proving its correctness at the machine code level. We present our verification strategy, which mixes the usage of the theorem prover HOL4, the computation of weakest preconditions, and the use of SMT solvers to largely automate the verification process. The automation relies on an integration of HOL4 with BAP, the Binary Analysis Platform developed at CMU. To enable the adoption of the BAP back-ends to compute weakest preconditions and control flow graphs, a HOL4-based tool was implemented that transforms ARMv7 assembly programs to the BAP Intermediate Language. Since verifying contracts by computing the weakest precondition depends on resolving indirect jumps, we implemented a procedure that integrates SMT solvers and BAP to discover all the possible assignments to the indirect jumps under the contract precondition.},
  Bibsource                = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:Journals/ics/afzali2012,
	Title                    = {Private Key Based Query on Encrypted Data},
	Author                   = {With: Hammad Afzali and Hamed Nemati and Reza Azmi},
	Journal                  = {Journal of THE ISC INTERNATIONAL Journal OF INFORMATION SECURITY},
	Year                     = {2012},
	Number                   = {1},
	Pages                    = {41--50},
	Volume                   = {4},
	
	Doi                      = {10.22042/isecure.2015.4.1.5},
	Url                      = {} %%{http://www.sid.ir/En/Journal/ViewPaper.aspx?ID=346694}
}

@InProceedings{ISCEE15_017,
	Title                    = {Reconstruction of OS Critical Data-Structure Using VMM},
	Author                   = {Hammad Afzali and Hamed Nemati and Reza Azmi},
	BookTitle                = {15th Iran Electrical Engeenring Conference, {ICEE} 2012, Iran, [In Farsi].},
	Year                     = {2012},
	
	Url                      = {https://bit.ly/2FnwLEy}
}

@InProceedings{DBLP:conf/worldcis/BorgheiAGN11,
	Title                    = {Virtual machine based security architecture},
	Author                   = {Elahe Borghei and Reza Azmi and Alireza Ghahremanian and Hamed Nemati},
	BookTitle                = {2011 World Congress on Internet Security, WorldCIS 2011, London, UK, February 21-23, 2011},
	Year                     = {2011},
	Pages                    = {210--215},
	
	Bibsource                = {dblp computer science bibliography, https://dblp.org},
	BibUrl                   = {https://dblp.org/rec/bib/conf/worldcis/BorgheiAGN11},
	Crossref                 = {DBLP:conf/worldcis/2011},
	Timestamp                = {Sat, 29 Apr 2017 01:00:00 +0200},
	Url                      = {http://ieeexplore.ieee.org/document/5749853/},
	Abstract                 = {In this paper a new approach based on using reference validation mechanism to improve system reliability is proposed. Since device drivers are the main cause of system failure, they are chosen as case study. Thus by improving driver reliability, security of the whole system is improved. To monitor driver functionality and also manage kernel memory, lightweight hypervisor layer is used, and reference validation mechanism is implemented in this layer.}
}

@InProceedings{ISCC07_031,
	Title                    = {Intrusion Detection Using VMM},
	Author                   = {Hamed Nemati and Reza Azmi and Alireza Ghahramanian},
	BookTitle                = {7th International ISC Conference on Information Security and Cryptology, {ISCC} 2010, Iran, [In Farsi].},
	Year                     = {2010},
	
	Url                      = {https://bit.ly/2ForuvE}
}

@InProceedings{DBLP:conf/icitst/RezaeiMNA10,
	Title                    = {TCvisor: {A} hypervisor level secure storage},
	Author                   = {Mohammad Rezaei and Nafise Sadat Moosavi and Hamed Nemati and Reza Azmi},
	BookTitle                = {5th International Conference for Internet Technology and Secured Transactions, {ICITST} 2010, London, United Kingdom, November 8-10, 2010},
	Year                     = {2010},
	Pages                    = {1--9},
	
	Bibsource                = {dblp computer science bibliography, https://dblp.org},
	BibUrl                   = {https://dblp.org/rec/bib/conf/icitst/RezaeiMNA10},
	Crossref                 = {DBLP:conf/icitst/2010},
	Timestamp                = {Sat, 29 Apr 2017 01:00:00 +0200},
	Url                      = {http://ieeexplore.ieee.org/document/5678529/},
	Abstract                 = {In this paper, we present design and implementation of TCvisor, a new trusted hypervisor. To this end, TCvisor provides a secure storage with different isolated view per user by using para-passthrough and combined key. In this regard, virtualization technology of processors has been used for complete isolation from operating system. By combining TPM base key, user's password and geo function key, TCvisor provides a secure storage in an environment with split data. We have applied feature wise security analysis TCvisor's secure storage from software system layers point then we have compared performance of TCvisor to selected candidates of existing layers.}
}