Spec Problem

[d1jang]

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?

[ztatlock]

I think the problem is just that the spec is incomplete.

The actual code does check the component type before dispatching to the correct handler.

So we need to update the spec generator...

[ztatlock]

@d1jang Why did you close this? Isn't it still an issue?

[d1jang]

This is still an issue. Sorry for the mistake!

[ztatlock]

Haha, no worries! I've accidentally closed / reopened several issues :)