#OKL4 #opensource to see what #NSA did to it

2: co.okl4-developer/cyb/sec/OKL4
/open source to see what NSA did to it:

Ph.T 8:57 PM to Jim, developer 
I think the problem is OKL4 is military-grade isolation,
and the NSA doesn't want us to be protected like that .

Daniel Potts danielp@ok-labs.com 9:20 PM to me, developer
Hi Ph. T,
I love the theory!  OKL4 is used for
many Information Assurance programs
- those that make it harder to hack
(irrespective of who you are).
They are also used in the same way
to improve safety, reliability, etc
across all sorts of connected and embedded devices.
I'm not sure what the point of this thread is,
other than to troll OKL.  However,
I am keen to hear some constructive ideas
(as well as conspiracy theories - love them!),
so I'd like to hear about what people are
actually wanting to do with OKL4.
What do you need/want?  What do you plan to build?
Product or academic?
As mentioned previously,
one of the major factors with lack of updates
under a liberal license for OKL4,
is lack of community involvement
such as contributions of new SoC ports, bug fixes,
demo systems, products, etc.
I don't want to discount that
many members of our community
have done some amazing work in the above categories,
but I suppose this open source program
has not gained enough momentum to be self sustaining.
We also had some people take the code and fork it off.
Again, while perhaps within their rights,
that isn't particularly helpful in the spirit of community.
We have kept OKL4 3.x available,
because our main past community involvement
was people wanting to look into a modern kernel,
and those were largely academic.
With OKL4 4.x and later,
we would like to explore
making it more widely available,
and to make a case for that
I am keen to hear more about
what you'd like to use it for.
my thoughts:
. it was only after I read this response to me
that I realized what I had really said:
only by having it closed-sourced,
can it accept obvious vulnerabilities from NSA .

my reply: 
I see that the open source security community
is rallying around Xen, (see Qubes OS)
as it supports unmodified kernels .
. however,
as has been pointed out by okL4 staff,
the Xen TCB is much larger than okL4,
making verification impractical,
in contrast to okL4 Verified .