[macs] Fwd: [Security-seminar] Talk (tentatively Thurs 9/22, 5-6 pm): Runtime path verification of web-based single sign-on implementations

Mayank Varia varia at bu.edu
Mon Sep 12 21:08:25 EDT 2016

FYI: the following talk may be of interest to the MACS community.

On a different note: most of the slides from Friday have been posted online
at http://www.bu.edu/macs/workshops/meeting-september-2016/. Also, if you
wish to sign up for an account at the MOC, you may do so by visiting


---------- Forwarded message ---------
From: Matt McCutchen <rmccutch at mit.edu>
Date: Mon, Sep 12, 2016 at 14:37
Subject: [Security-seminar] Talk (tentatively Thurs 9/22, 5-6 pm): Runtime
path verification of web-based single sign-on implementations
To: <pl at csail.mit.edu>, <systems-security at csail.mit.edu>

Dear PL/SE and security groups,

I'll give a talk that may be of interest to people in both groups (see
below), but not in either the PL/SE seminar or the security seminar because
of schedule conflicts.  The talk is tentatively scheduled for Thursday,
September 22, 5-6 pm (a Software Design Group meeting slot).  If you are
interested in attending but cannot make this time, *please let me know by
the end of tomorrow* so I can look for another time; sending me such a
message is not a commitment to attend.  I'll announce the final time later
this week.

Thanks for your attention,

Title: Runtime path verification of web-based single sign-on implementations


Web-based single sign-on protocols such as OpenID Connect let a user use an
account on an identity provider web site (e.g., Microsoft) to log into
third-party web sites, called relying parties.  These protocols intend to
achieve two basic security properties: no one can log in to a relying party
as a user Alice without her cooperation (login safety), nor can Alice be
caused to log in as another user without her cooperation (login intent).
Unfortunately, implementations often have security bugs in which the checks
they perform are insufficient to guarantee these properties.  We describe
SVAuth, a C# framework for single sign-on implementations that verifies
these properties at runtime across a multiparty system with only modest
additional work by the developer, in contrast to existing techniques.  The
developer identifies critical methods that contain the core protocol
logic.  On each protocol run, SVAuth automatically records the sequence of
critical methods executed across all parties and verifies symbolically that
this sequence of methods guarantees the security properties, under a model
that assumes that the rest of the code obeys certain straightforward
rules.  With this approach, we can verify properties that refer to model
variables not available at runtime without needing to analyze the whole
implementation.  The key concept that allows a relationship between clients
of the identity provider and of the relying party to be deduced from
specific security checks is that of a secret, which is only allowed to be
sent to a specified list of parties and authenticates anyone who bears it
as one of those parties.  We've developed SVAuth-based relying party
implementations for several popular identity providers (Facebook, Google,
Microsoft, and Yahoo) and are working with several relying party web sites
interested in adopting SVAuth on an experimental basis.

Systems-security mailing list
Systems-security at lists.csail.mit.edu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs-mailman.bu.edu/pipermail/macs-announce/attachments/20160913/1aa1f69a/attachment.html>

More information about the macs-announce mailing list