Model the CSP sandbox

[lsd-cat]

The current CSP sandbox is based on my understanding of the CSP spec, but we know I missed some that could have allowed for bypasses, etiher because of inheritances or different type of sources. Would be nice if we modeled the CSP spec in something like z3, then my validating function, and then we solved to look for javascript/css/objects execution vectors.

[cfm]

Some prior art that might offer interesting approaches if not anything concrete we can reuse:

• Calzavara et al. (2019), "Semantically Sound Analysis of Content Security Policies"
• Calzavara et al. (2020), "A Tale of Two Headers: A Formal Analysis of Inconsistent Click-Jacking Protection on the Web"
• Veronese et al. (2022), "WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms"