PLDI 2013

Security Properties

SSH

1. Access control for pseudo terminal: never exec pseudo terminal process until user has authenticated.

  // c is password checking component (chan to System)
  (.*[recv c (Auth user "true")])?[^spawn AllocPTY user]*

1. Limit password checking attempts: slave cannot attempt authentication more than 3 times.

  // c is password checking component (chan to System)
  (.*[send c (Auth user pass)]
   .*[send c (Auth user pass)]
   .*[send c (Auth user pass)]
   .*[send c (Auth user pass)]
   .*)!

Quark

1. Tab non-interference : a tab cannot affect the way that the kernel interacts with other tabs.

  ???

1. Cookie confidentiality & integrity : cookies for a domain can only be accessed by tabs of that domain.

  This will depend on per-component state.
  Can we use ImmBefore and ImmAfter for this?
  Should we stick with regular expression?

  // Don's first draft of this property
  (^.*(Exec "tab.py" ?tdomain ?tchan).*
  (Exec "cookie.py" ?cdomain ?cchan).*
  (RecvMsg ?tchan ?str).*
  (SendMsg ?cchan ?str)) ==> (?tdomain = ?cdomain)

1. Address bar correctness : the address bar cannot be modified by a tab without the user being involved, and always displays the correct address bar.

  This will depend on per-component state.
  Can we use ImmBefore and ImmAfter for this?
  Should we stick with regular expression?

  // Don's first draft of this property
  ^.*(Exec "stdout.py" ?achan).*(Exec "stdin.py" ?uchan).*
  [^ SendMsg ?achan ?]*(RecvMsg ?uchan ?)