Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Security '12 Home
  • Registration Information
  • Registration Discounts
  • Organizers
  • At a Glance
  • Calendar
  • Technical Sessions
  • Workshops
  • Hotel & Travel Information
  • Poster Session
  • Rump Session
  • Birds-of-a-Feather Sessions
  • Sponsors
  • Activities
  • Students
  • Questions?
  • For Participants
  • Help Promote
  • Call for Papers
  • Past Proceedings

sponsors

Gold Sponsor
Silver Sponsor
Silver Sponsor
Bronze Sponsor
Bronze Sponsor
Bronze Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor

twitter

Tweets by USENIXSecurity

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home » Establishing Browser Security Guarantees through Formal Shim Verification
Tweet

connect with us

http://twitter.com/USENIXSecurity
https://www.facebook.com/events/309825352408177/

Establishing Browser Security Guarantees through Formal Shim Verification

Authors: 

Dongseok Jang, Zachary Tatlock, and Sorin Lerner, University of California, San Diego

Abstract: 

Web browsers mediate access to valuable private data in domains ranging from health care to banking. Despite this critical role, attackers routinely exploit browser vulnerabilities to exfiltrate private data and take over the underlying system. We present QUARK, a browser whose kernel has been implemented and verified in Coq. We give a specification of our kernel, show that the implementation satisfies the specification, and finally show that the specification implies several security properties, including tab non-interference, cookie integrity and confidentiality, and address bar integrity.

Dongseok Jang, University of California, San Diego

Zachary Tatlock, University of California, San Diego

Sorin Lerner, University of California, San Diego

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {180207,
author = {Dongseok Jang and Zachary Tatlock and Sorin Lerner},
title = {Establishing Browser Security Guarantees through Formal Shim Verification},
booktitle = {21st USENIX Security Symposium (USENIX Security 12)},
year = {2012},
isbn = {978-931971-95-9},
address = {Bellevue, WA},
pages = {113--128},
url = {https://www.usenix.org/conference/usenixsecurity12/technical-sessions/presentation/jang},
publisher = {USENIX Association},
month = aug,
}
Download
Jang PDF
View the slides

Presentation Video

Presentation Audio

MP3 Download OGG Download

Download Audio

  • Log in or    Register to post comments

Gold Sponsors

Silver Sponsors

Bronze Sponsors

Media Sponsors & Industry Partners

© USENIX

  • Privacy Policy
  • Contact Us