WebSpec, a formal framework for browser security analysis, reveals new cookie attack

Boffins in Vienna devise way to make software prove how it behaves

Folks at Technische Universität Wien in Austria have devised a formal security framework called WebSpec to analyze browser security.

And they've used it to identify multiple logical flaws affecting web browsers, revealing a new cookie-based attack and an unresolved Content Security Policy contradiction.

These logical flaws are not necessarily security vulnerabilities, but they can be. They're inconsistencies between Web platform specifications and the way these specs actually get implemented within web browsers.

WebSpec was developed by Lorenzo Veronese, Benjamin Farinier, Mauro Tempesta, Marco Squarcina, Matteo Maffei in an effort to bring rigor to web security through automated, verifiable rule checking rather than manual evaluation.

Browsers, as they explain in an academic paper, "WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms," have become tremendously complex and continue to become more so as additional components get added to the web platform.

New web platform components undergo compliance testing, the researchers say, but their specifications get reviewed manually by technical experts to understand how new technologies interact with legacy APIs and individual browser implementations.

"Unfortunately, manual reviews tend to overlook logical flaws, eventually leading to critical security vulnerabilities," the computer scientists explain, pointing to how eight years after the introduction of the HttpOnly flag in Internet Explorer 6 – as a way to keep cookies confidential from client-side scripts – researchers discovered the flag could be bypassed by scripts accessing the response headers of an AJAX request using the getResponseHeader function.

WebSpec uses the Coq theorem proving language to subject the interplay of browsers and their specified behavior to formal testing. It makes browser security a matter of machine-checkable Satisfiability Modulo Theories (SMT) proofs [PDF].

To test for inconsistencies between web specs and browsers, the researchers defined ten "invariants," each of which describes "a property of the Web platform that is expected to hold across its updates and independently on how its components can possibly interact with each other."

These invariants or rules represent testable conditions that should hold true, such as "Cookies with the Secure attribute can only be set (using the Set-Cookie header) over secure channels," as defined in RFC 6265, Section

Of the ten invariants evaluated, three failed.

"In particular, we show how WebSpec is able to discover a new attack on the __Host- prefix for cookies as well as a new inconsistency between the inheritance rules for the Content Security Policy and a planned change in the HTML standard," the paper explains.

HTTP cookies prefixed with "__Host-" are supposed to only be set by the host domain or scripts included on pages on that domain. WebSpec, however, found an attack to break the related invariant test.

"A script running on a page can modify at runtime the effective domain used for SOP [Same-Origin Policy] checks through the document.domain API," the paper explains, noting that the mismatch between access control policies in the Document Object Model and the cookie jar lets a script running in an iframe access the document.cookie property on a parent page if both pages set document.domain to the same value.

The researchers note that while the current web platform remains vulnerable to this attack, eventually it won't be: The document.domain property has been deprecated, meaning future browser updates will omit support, some day.

The authors also used WebSpec to discover an inconsistency with the way Blob objects – objects containing data that can be read as text, binary, or streams using built-in object methods – inherit their Content Security Policy.

Lorenzo Veronese, a doctoral student at TU Wien, raised the issue last July to the working group of the HTML standard, but the different behaviors described in the CSP spec and the policy container explainer have yet to be reconciled.

Antonio Sartori, a Google software engineer, has developed a fix but it has yet to be integrated into the HTML standard.

In any event, the availability of WebSpec as a tool to formally evaluate browser behavior should make life a bit easier for those struggling to maintain sprawling browser codebases. ®

Other stories you might like

  • UK government opens consultation on medic-style register for Brit infosec pros

    Are you competent? Ethical? Welcome to UKCSC's new list

    Frustrated at lack of activity from the "standard setting" UK Cyber Security Council, the government wants to pass new laws making it into the statutory regulator of the UK infosec trade.

    Government plans, quietly announced in a consultation document issued last week, include a formal register of infosec practitioners – meaning security specialists could be struck off or barred from working if they don't meet "competence and ethical requirements."

    The proposed setup sounds very similar to the General Medical Council and its register of doctors allowed to practice medicine in the UK.

    Continue reading
  • Microsoft's do-it-all IDE Visual Studio 2022 came out late last year. How good is it really?

    Top request from devs? A Linux version

    Review Visual Studio goes back a long way. Microsoft always had its own programming languages and tools, beginning with Microsoft Basic in 1975 and Microsoft C 1.0 in 1983.

    The Visual Studio idea came from two main sources. In the early days, Windows applications were coded and compiled using MS-DOS, and there was a MS-DOS IDE called Programmer's Workbench (PWB, first released 1989). The company also came up Visual Basic (VB, first released 1991), which unlike Microsoft C++ had a Windows IDE. Perhaps inspired by VB, Microsoft delivered Visual C++ 1.0 in 1993, replacing the little-used PWB. Visual Studio itself was introduced in 1997, though it was more of a bundle of different Windows development tools initially. The first Visual Studio to integrate C++ and Visual Basic (in .NET guise) development into the same IDE was Visual Studio .NET in 2002, 20 years ago, and this perhaps is the true ancestor of today's IDE.

    A big change in VS 2022, released November, is that it is the first version where the IDE itself runs as a 64-bit process. The advantage is that it has access to more than 4GB memory in the devenv process, this being the shell of the IDE, though of course it is still possible to compile 32-bit applications. The main benefit is for large solutions comprising hundreds of projects. Although a substantial change, it is transparent to developers and from what we can tell, has been a beneficial change.

    Continue reading
  • James Webb Space Telescope has arrived at its new home – an orbit almost a million miles from Earth

    Funnily enough, that's where we want to be right now, too

    The James Webb Space Telescope, the largest and most complex space observatory built by NASA, has reached its final destination: L2, the second Sun-Earth Lagrange point, an orbit located about a million miles away.

    Mission control sent instructions to fire the telescope's thrusters at 1400 EST (1900 UTC) on Monday. The small boost increased its speed by about 3.6 miles per hour to send it to L2, where it will orbit the Sun in line with Earth for the foreseeable future. It takes about 180 days to complete an L2 orbit, Amber Straughn, deputy project scientist for Webb Science Communications at NASA's Goddard Space Flight Center, said during a live briefing.

    "Webb, welcome home!" blurted NASA's Administrator Bill Nelson. "Congratulations to the team for all of their hard work ensuring Webb's safe arrival at L2 today. We're one step closer to uncovering the mysteries of the universe. And I can't wait to see Webb's first new views of the universe this summer."

    Continue reading

Biting the hand that feeds IT © 1998–2022