Formal Security Analysis of Widevine through the W3C EME Standard

Stéphanie Delaune, Joseph Lallemand, Gwendal Patat, Florian Roudot, and Mohamed Sabt. Formal Security Analysis of Widevine through the W3C EME Standard. In Proceedings of the 33rd USENIX Security Symposium, (USENIX'24), USENIX Association, Philadelphia, PA, USA, 2024.

Download

[PDF] 

Abstract

Streaming services such as Netflix, Amazon Prime Video, or Disney+ rely on the widespread EME standard to deliver their content to end users on all major web browsers. While providing an abstraction layer to the underlying DRM protocols of each device, the security of this API has never been formally studied. In this paper, we provide the first formal analysis of Widevine, the most deployed DRM instantiating EME.We define security goals for EME, focusing on media protection and usage control. Then, relying on the TAMARIN prover, we conduct a detailed security analysis of these goals on some Widevine EME implementations, reverse-engineered by us for this study. Our investigation highlights a vulnerability that could allow for unlimited media consumption. Additionally, we present a patched protocol that is suitable for both mobile and desktop platforms, and that we formally proved secure using TAMARIN.

BibTeX

@inproceedings{DLPRS-usenix24,
  editor = {Davide Balzarotti and Wenyuan Xu},
abstract = {Streaming services such as Netflix, Amazon Prime Video, or Disney+ rely on the widespread EME standard 
to deliver their content to end users on all major web browsers. While providing an abstraction layer to the underlying 
DRM protocols of each device, the security of this API has never been formally studied. In this paper, we provide 
the first formal analysis of Widevine, the most deployed DRM instantiating EME.
We define security goals for EME, focusing on media protection and usage control. Then, relying on the TAMARIN prover, 
we conduct a detailed security analysis of these goals on some Widevine EME implementations, reverse-engineered by us for this study. 
Our investigation highlights a vulnerability that could allow for unlimited media consumption. 
Additionally, we present a patched protocol that is suitable for both mobile and desktop 
platforms, and that we formally proved secure using TAMARIN.},
  author       = {St{\'{e}}phanie Delaune and Joseph Lallemand and Gwendal Patat and Florian Roudot and Mohamed Sabt},
  title        = {{F}ormal {S}ecurity {A}nalysis of {W}idevine through the {W3C} {EME} {S}tandard},
  booktitle    = {{P}roceedings of the 33rd {USENIX} Security Symposium, ({USENIX}'24)},
 address = {Philadelphia, PA, USA},
  OPTpages        = {},
  publisher    = {{USENIX} Association},
  year         = {2024},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}