Security Properties Encoded In CTL or Regex?

[d1jang]

Hi all--

I've come up with a couple of security properties for SSH and
Quark.

Here, the state machine (where the formula is proved against) is
defined in a way that each state is corresponding to a primitive
action generated by the kernel. A formula is an action, and it is
evaluated to true when the current state's action is matched with the
formula.

• CTL Formula
• A e - e is true all along the pathes from the current state.
• EF e - e is true at least on one path from now on in the future.
• A (e1 U e2) - from now one, e1 is true until e2 becomes true.

I realized that we can encode some CTL formulas in regular expressions
which are matched with our traces. This might be totally nonsense, but
I've tried to transform CTL formula I've come up with to a regular
expression. [^ e] mached with a string which doesn't contain e, and ~~
(e) matched with a string which does NOT match with e (so, ~~ is a
complement operator here), and for regex ^e, ^ stands for the
beginning of a line.

=== SSH

1. Access control for pseudo terminal creation

A pseudo terminal process cannot be executed until authentication is
successfully done.

CTL : A ((~ Exec "ptyer.py" ?user) U (Auth ?user true))
REGEX : ^[^ Exec "ptyer.py" ?user]+(Auth user ?true)

1. Limited number of password checking

The slave cannot try authentication more than 3 time.

CTL : ~ EF((Auth ? ?) -> EF((Auth ? ?) -> EF((Auth ? ?) -> EF(Auth ? ?))))
REGEX : ~~(^.(Auth ? ?).(Auth ? ?).(Auth ? ?).(Auth ? ?))

=== Quark

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

?? DON'T KNOW!! IS IT POSSIBLE??

1. cookie confidentiality & integrity : cookies for a domain can only
   be accessed by tabs of that domain. So here the intutiion is that
   whenever something is sent to a cookie process, that something must be from
   a tab whose domain is the same as the cookie process's one.

CTL: EF((Exec "tab.py" ?tdomain ?tchan) -> EF((Exec "cookie.py"
?cdomain ?cchan) -> EF ((RecvMsg ?tchan ?str) -> EF (SendMsg ?cchan
?str)))) ==> (?tdomain = ?cdomain)

REGEX:
(^.(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. Here, the intuition is that before something is read from
   the user(stdin), nothing can be written to the screen(stdout).

CTL:
EF((Exec "stdout.py" ?achan)
-> EF((Exec "stdin.py" ?uchan)
-> A ( ~(SendMsg ?achan ?) U (RecvMsg ?uchan ?))))

REGEX:
^.(Exec "stdout.py" ?achan).(Exec "stdin.py" ?uchan).*
[^ SendMsg ?achan ?]*(RecvMsg ?uchan ?)