[cap-talk] cap patterns in 1ml

[Matt Rice]

hi so i've been trying to apply cap patterns to 1ml,

I posted a repository of various things here..

https://gitlab.com/ratmice/1ml-stuff/tree/master
https://gitlab.com/ratmice/1ml-stuff

currently just includes attenuation (in ref.1ml)
and the sealer/unsealer thing i'd posted earlier...

but there is some other non-cap stuff like a type for value discrimination,
and other random junk
the prototype 1ml compiler and papers are available from

https://www.mpi-sws.org/~rossberg/1ml/

[Matt Rice]

so, I'm going to attempt to describe my thoughts on 1ml and how it relates to cap's

as it is almost certainly not the object capability model..

"In a system where designation and authority are inseparable, this common type of confused deputy problem – in which a malicious party designates a resource they are not supposed to access – simply cannot occur."

"If designators are inseparable from authorities, any request for access must necessarily include the authority"

from the capability myths demolished,

1ml differs in that It doesn't exactly have objects in the traditional sense of a pair of state and behaviour which are inseparable... It has a primitive reliance on synergy
where a value of some type gives no authority except to have it.

similarly a function which accepts a parameter of some type, is not callable without a value of that type, and thus gives no authority.

so through synergy on types and functions accepting things of those types you get the state/behaviour pair... It should be obvious that this doesn't really extend to cases

where you have multiple values sharing types.  which is certainly something to be wary of.

using some terms from here:
http://cap-lore.com/CapTheory/term.html

types being values, the general local scoping allows for veiling and defending I believe..

I haven't quite gotten to factories yet, but my theory is that the holes in a factory, are quite reminiscent of what 1ml calls 'large types', and so by bringing together two large types, or opaque types, together with a translucent interface to the type, through currying...

Not quite there yet honestly, the basic file metaphor of source files makes it a bit odd to express disjoint environments, without separate compilation.

and FWIW, the descrim type and the descrim key from keykos don't really match up, it seems like the keykos descrim implemented in this descrim

would be something that if it type checks returns true (not particularly more useful than just a normal type annotation)

[Matt Rice]

On Tue, Jan 19, 2016 at 7:45 PM, Matt Rice <rat...@gmail.com> wrote:
>
> I haven't quite gotten to factories yet,

Well I am skeptical that types & pure constructors alone is going to
be able to confine now primarily because I don't believe the effects
of a monad within in a pure constructor are going to be confined to
the pure constructor, without some form of environment restriction
e.g. the usual ways
_______________________________________________
cap-talk mailing list
cap-...@mail.eros-os.org
http://www.eros-os.org/mailman/listinfo/cap-talk

[Raoul Duke]

On Sun, Jan 24, 2016 at 1:48 PM, Matt Rice <rat...@gmail.com> wrote:
> On Tue, Jan 19, 2016 at 7:45 PM, Matt Rice <rat...@gmail.com> wrote:
>> I haven't quite gotten to factories yet,
> Well I am skeptical that types & pure constructors alone is going to
> be able to confine now primarily because I don't believe the effects
> of a monad within in a pure constructor are going to be confined to
> the pure constructor, without some form of environment restriction
> e.g. the usual ways

Is there a good example anywhere of how to get that level of security
in a language? Thanks.

[Matt Rice]

On Mon, Jan 25, 2016 at 12:19 PM, Raoul Duke <rao...@gmail.com> wrote:
> On Sun, Jan 24, 2016 at 1:48 PM, Matt Rice <rat...@gmail.com> wrote:
>> On Tue, Jan 19, 2016 at 7:45 PM, Matt Rice <rat...@gmail.com> wrote:
>>> I haven't quite gotten to factories yet,
>> Well I am skeptical that types & pure constructors alone is going to
>> be able to confine now primarily because I don't believe the effects
>> of a monad within in a pure constructor are going to be confined to
>> the pure constructor, without some form of environment restriction
>> e.g. the usual ways
>
>
> Is there a good example anywhere of how to get that level of security
> in a language? Thanks.

a good example I think is
Jonathan Rees Security Kernel for the lambda calculus
http://mumble.net/~jar/pubs/secureos/

I noticed he recently posted a repository for it on github here
https://github.com/jar398/w7

I guess my question was can we get this without mucking about with
first class environments?
instead using the type system and I think it boils down to sort of,
if you add the set of free/non-local variables as a part of a
functions type, or (at least)
allow the language to discriminate between combinators (which have no
free/non-local variables)
and other functions with free variables.

[Matt Rice]

On Mon, Jan 25, 2016 at 1:17 PM, Matt Rice <rat...@gmail.com> wrote:

>
> I guess my question was can we get this without mucking about with
> first class environments?
> instead using the type system and I think it boils down to sort of,
> if you add the set of free/non-local variables as a part of a
> functions type, or (at least)
> allow the language to discriminate between combinators (which have no
> free/non-local variables)
> and other functions with free variables.

I should have probably extrapolated on this,

foo 'a 'b (state:a) (constructor:a => b) = constructor(state)

so via 'a => b' a is pure, it can't smuggle anything out at
constructor call time.

foo 'a 'b (state:a) (constructor:a ={}> b) = constructor(state)

or some syntax where ={}> denotes pure combinator, it can't steal anything at
constructor time, and it contains no free variables that can be used to
smuggle anything at post-constructor foo(...).something(...) call time.

the main concern with this is 'state', any read-write references
provided in state
may have a reference to a reference stowed away, similarly any
function in 'state'
should be a combinator...

there is a chicken/egg problem though such that some oracle is
required to protect predecessors from successors or a trusted 3rd
party, or human scrutiny of the types as-per above,

hence the name 'foo' rather than 'factory'. I'm not sure exactly what
should be done about state (if anything)

but the general idea is that 'a and state (of type a) denote the
innards 'b' describes the types of parameters and return values that
can enter/escape, and constructor constructs some kind of a 'b' to
interact with using what it gets from state...
both parties in general agree to some terms about 'a and 'b.

anyhow...