ucsd-pl / kraken Goto Github PK

Python and C libs should use "kraken_" prefix to avoid name collisions.

Working on fixing that.

@ztatlock

Num(a, b) or Num a b?

low then high, or high then low?

cf. d5309fb and b272390

This code crashes the compiler

Msg(some_val) {
state_var := some_val;
}

The problem happens sstate is not initialized with a message handler's arguments(payloads).
A quick fix can solve the problem.

When the tactic faces with this goal:

KTraceMatch (KTP_NegClass (KAP_KRecv MP_M :: nil))
(KRecv c (BadTag tag) :: nil)

It applies KTM_NegClass, and results in the following goal :

forall kap : KActionPat,
In kap (KAP_KRecv MP_M :: nil) ->
~ KActionMatch kap (KRecv c (BadTag tag))

But ktm_basic doesn't deal with this shape of goal.

Our kernel specification has a problem that lets a component of type A can freely call message handlers that belong to components of type B.

Here's the problem. The specification doesn't mention the component type that executes a message handler as follows :

| VE_Main_M_0 :
forall y c,
ValidExchange (mkst comps
(tr ~~~ ((Exec_t (string2str "test.py") c2 ++ SendMsg c (M (("H" :: "E" :: "L" :: "L" :: "O" :: nil))) ++ RecvMsg c (M y)) ++ tr))
)

As you can see, it doesn't check anything on c, the channel used for this communication. This can cause a problem that different components are allowed for different capabilities.

Imagine that a component A can obtain secret data from the kernel as free as it wants by calling event handler H1. We want another component B not to be able to do that. But our spec doesn't say anything about it. So even a program verified to follow the spec can leak secret data to any components. Therefore, we're not going to prove security properties without fixing this problem since we can't discriminate different components now.

A solution is simple : to add meta data to signify which channel is to whom, and maintain that information in the kernel state. So the spec will look like this :

| VE_Main_M_0 :
forall y c c2,
In c comps ->
Typeof kst c MainType ->
ValidExchange (mkst c2::comps
(tr ~~~ ((Exec_t (string2str "test.py") c2 ++ SendMsg c (M (("H" :: "E" :: "L" :: "L" :: "O" :: nil))) ++ RecvMsg c (M y)) ++ tr))
)

I'm planning to fix this problem after finishing whenclause stuff.
Any thoughts on this?

1: encode \n on python side

2: name using FD - 1 (is that safe?)

3: python should flush on log()

For now, my "quick fix" has been to always put all components in Exchange, even the ones with no handler.

genCoq should check the missing components and generate exchange_ for the ones missing.

@ztatlock The maximum 3 login trial policy failed.
You can checkout the regexp-test branch, and try to compile u-ssh.

The tactic cannot match a regular expression describing a trace containing exactly 3 login trials with a trace generated by KInvariant.

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 ?)

The following init code:

Init {
  output := spawn(Output);
  send(output, "?");
}

produces the following, erroneous code:

Inductive KInvariant : kstate -> Prop :=
| KT_init :
  forall output output,
    KInvariant (mkst (output :: nil) [SendMsg output (K2GDisplay (("?" :: nil))) ++ Exec_t (string2str "../../../home/ucsd/vcr/python-browser-8/output.py") output ++ nil] (output))

since output is quantified twice.

A same name is used for multiple variables of the same type, and the problem occurs because we're using variables' type as their binding names here.

| VE_System_CreatePtyerRes: forall fdesc fdesc c, ValidExchange (mkst ...)

Running the full test suite just took me over 10 minutes.

All tests take at least 30 seconds.

Too slow!

The kraken compiler uses hardcoded vars in several places which can lead to confusing errors in the case of name collisions.

The tests in state-00 have not been updated to the change in the Python messaging interface.

send_msg should become send
recv_msg should become recv

This should be fixed somewhere at some point.

very lacking right now

Components who do not have any message handler don't get any ValidExchange constructor generated, thus preventing proofs from going through.

The quick & dirty fix is to add empty handlers in the kernel.krn.

When I tried to make a message type Msg(fdesc, fdesc), the compiler generates the following spec :

forall fdesc fdesc c, ValidExchange (mkst comps (tr ~~~ (RecvMsg c (CreatePtyerRes fdesc fdesc) ++ tr)) system

The compiler needs to generate different names.

I'm going to fix this problem as soon as Zach pulls the new cleanup into master.

@d1jang @Ptival We have a lot of old branches sitting around.

Is it OK to delete these branches?
stateful
ssh-proto
components
ifexp
u-quark
whenclause
fix

They all appear to be merged into master and I don't think there's any active development on any of them...

@d1jang @Ptival

In https://github.com/UCSD-PL/kraken/blob/master/compiler/bin/kraken.sh "ocamldebug" was changed to "ocamlrun".

Was there a reason for this change?

I'd rather have debug, so unless someone feels strongly, I'm going to change it back.

AlwaysResponds =
ImmAfter {
"KRecv chan msg :: nil"
}{
"KSend chan msg :: nil"
};

AlwaysRespondsRegex =
Match {
([^recv M]|([send M][recv M]))*
};

OnlyResponds =
ImmBefore {
"KRecv chan msg :: nil"
}{
"KSend chan msg :: nil"
};

OnlyRespondsRegex =
Match {
([^send M]|([send M][recv M]))*
};

In https://github.com/UCSD-PL/kraken/blob/master/compiler/test/when-00/kernel.krn

Shouldn't the == 5 handler either:

• not increment the counter
• or be >= 5
  ?

@d1jang can you explain more about trace_impl vs. trace_spec?

The problem is that this line of code:

curtab := spawn

compiles down to:

curtab <- exec Tab (str_of_string "/home/ucsd/vcr/python-browser-8/tab.py")
(tr ~~~ expand_ktrace (KRecv c (Navigate url) :: tr))
<@> [In curtab comps] * [In output comps] * all_bound comps * [In c comps] * (tr ~~ [KInvariant kst]) * emp;

which capturs curtab in such a way that the goal [In curtab comps] now refers to the new curtab which is actually not in comps.

@ztatlock suggested a fix that I am going to try now: we need to update comps to (curtab :: comps) from that point on.

For old-quark, it would help if I could use absolute paths for components. Unfortunately, it gets compiled to:

/tmp/old-quark/client//home/ucsd/vcr/python-browser-8/input.py