Modelling and Verification of Security-Oriented Resource Partitioning Schemes

Adwait Godbole, Leiqi Ye, Yatin A. Manerkar, and Sanjit A. Seshia. Modelling and Verification of Security-Oriented Resource Partitioning Schemes. In International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 268–273, IEEE, 2023.

Download

[HTML] 

Abstract

Side channel attacks such as Spectre and Meltdown exploit on-chip resources such as caches and buffers sharedbetween the victim and the attacker in order to leak secret information from the victim. Previous works aim to mitigatethese attacks by partitioning these vulnerable resources and allocating disjoint partitions to mutually untrusting processdomains. While disjoint allocation prevents the attacker from gaining direct visibility of victim's partitions, secret informationcan also be leaked through the book-keeping state implementing the replacement/allocation policy. Proofs of security must reasonabout the partitions as well as the policy.<p>In this work, we develop an abstract formal model for a generic security-oriented resource partitioning scheme, and formulatea corresponding attacker model. We then develop conditional equality-based relational invariants that enable unbounded proofsof security of the partitioning scheme with respect to the attacker model. These invariants allow us to reason about the state ofthe partitioning policy, which, as we discuss, can be more challenging than reasoning about the partitions themselves. We useour framework to model two resource partitioning approaches: DAWG and COLORIS. We demonstrate that using our invariantsleads to verification performance improvements over other, more automated, model-checking approaches such as BMC and PDR.

BibTeX

@inproceedings{godbole-fmcad23,
  author       = {Adwait Godbole and
                  Leiqi Ye and
                  Yatin A. Manerkar and
                  Sanjit A. Seshia},
  editor       = {Alexander Nadel and
                  Kristin Yvonne Rozier},
  title        = {Modelling and Verification of Security-Oriented Resource Partitioning
                  Schemes},
  booktitle    = {International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
  pages        = {268--273},
  publisher    = {{IEEE}},
  year         = {2023},
  abstract = {Side channel attacks such as Spectre and Meltdown exploit on-chip resources such as caches and buffers shared
between the victim and the attacker in order to leak secret information from the victim. Previous works aim to mitigate
these attacks by partitioning these vulnerable resources and allocating disjoint partitions to mutually untrusting process
domains. While disjoint allocation prevents the attacker from gaining direct visibility of victim's partitions, secret information
can also be leaked through the book-keeping state implementing the replacement/allocation policy. Proofs of security must reason
about the partitions as well as the policy.
<p>
In this work, we develop an abstract formal model for a generic security-oriented resource partitioning scheme, and formulate
a corresponding attacker model. We then develop conditional equality-based relational invariants that enable unbounded proofs
of security of the partitioning scheme with respect to the attacker model. These invariants allow us to reason about the state of
the partitioning policy, which, as we discuss, can be more challenging than reasoning about the partitions themselves. We use
our framework to model two resource partitioning approaches: DAWG and COLORIS. We demonstrate that using our invariants
leads to verification performance improvements over other, more automated, model-checking approaches such as BMC and PDR.},
}