Formal Verification of Browser Fingerprinting and Mitigation with Inlined Reference Monitors

Browser fingerprinting is a technique that identifies user devices by exploiting differences in software and hardware configurations. This technique is used in both benign applications, such as multi-factor authentication, and malicious ones, like web tracking and the disclosure of private information. Existing work has proposed various defense mechanisms against malicious browser fingerprinting and evaluated them using empirical experiments and analysis. While this approach demonstrates the effectiveness of mitigation methods, it does not provide proof of reliability. As browser fingerprinting research continues to advance and gain popularity across the web, there is an increasing need to verify the safety of user data and the reliability of protection mechanisms. In this paper, we develop formal models of both a browser fingerprinting tool and a controller capable of enforcing fingerprinting mitigation techniques. Specifically, we model an Inlined Reference Monitor for a canvas fingerprinter that intercepts JavaScript function calls and provides runtime policy enforcement. Our framework is highly extensible, allowing it to model a wide range of fingerprinting strategies and defenses. Using Computation Tree Logic, we formally define safety and liveness properties, demonstrating that our model successfully enforces key anti-fingerprinting techniques, such as randomization and API blocking.