Re: cap patterns in 1ml

--===============4143957067158934932==
Content-Type: multipart/alternative; boundary=001a11c2eb5aed7cd60529bbd02d

--001a11c2eb5aed7cd60529bbd02d
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

On Sat, Jan 16, 2016 at 6:11 PM, Matt Rice <[email protected]> wrote:

> 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 discriminatio=
n,
> and other random junk
> the prototype 1ml compiler and papers are available from
>
> https://www.mpi-sws.org/~rossberg/1ml/
>

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 =E2=80=93 in which a malicious party design=
ates a
resource they are not supposed to access =E2=80=93 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)

--001a11c2eb5aed7cd60529bbd02d
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><br><div class=3D"gmail_extra"><br><div class=3D"gmail_quo=
te">On Sat, Jan 16, 2016 at 6:11 PM, Matt Rice <span dir=3D"ltr">&lt;<a hre=
f=3D"mailto:[email protected]" target=3D"_blank">[email protected]</a>&gt;<=
/span> wrote:<br><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px =
0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=
=3D"ltr"><div>hi so i&#39;ve been trying to apply cap patterns to 1ml,<br><=
/div>I posted a repository of various things here..<br><div><div><br><a hre=
f=3D"https://gitlab.com/ratmice/1ml-stuff/tree/master" target=3D"_blank">ht=
tps://gitlab.com/ratmice/1ml-stuff/tree/master</a><br><a href=3D"https://gi=
tlab.com/ratmice/1ml-stuff" target=3D"_blank">https://gitlab.com/ratmice/1m=
l-stuff</a><br><br></div><div>currently just includes attenuation (in ref.1=
ml) <br>and the sealer/unsealer thing i&#39;d posted earlier...<br><br></di=
v><div>but there is some other non-cap stuff like a type for value discrimi=
nation,<br>and other random junk<br>the prototype 1ml compiler and papers a=
re available from<br><br><a href=3D"https://www.mpi-sws.org/~rossberg/1ml/"=
 target=3D"_blank">https://www.mpi-sws.org/~rossberg/1ml/</a><br></div></di=
v></div></blockquote><div><br></div><div>so, I&#39;m going to attempt to de=
scribe my thoughts on 1ml and how it relates to cap&#39;s<br></div><div>as =
it is almost certainly not the object capability model..<br><br>&quot;In a =
system where designation and authority are inseparable,=20
this common type of confused deputy problem =E2=80=93
in which a malicious party designates a resource
they are not supposed to access =E2=80=93
simply cannot occur.&quot;<br><br>&quot;If designators are inseparable from=
 authorities, any request for access must necessarily include the authority=
&quot;<br><br></div><div>from the capability myths demolished,<br><br></div=
><div>1ml differs in that It doesn&#39;t exactly have objects in the tradit=
ional sense of a pair of state and behaviour which are inseparable... It ha=
s a primitive reliance on synergy<br>where a value of some type gives no au=
thority except to have it.<br><br></div><div>similarly a function which acc=
epts a parameter of some type, is not callable without a value of that type=
, and thus gives no authority.<br></div></div><br></div><div class=3D"gmail=
_extra">so through synergy on types and functions accepting things of those=
 types you get the state/behaviour pair... It should be obvious that this d=
oesn&#39;t really extend to cases<br></div><div class=3D"gmail_extra">where=
 you have multiple values sharing types.=C2=A0 which is certainly something=
 to be wary of.<br></div><div class=3D"gmail_extra"><br>using some terms fr=
om here:<br><a href=3D"http://cap-lore.com/CapTheory/term.html">http://cap-=
lore.com/CapTheory/term.html</a><br><br></div><div class=3D"gmail_extra">ty=
pes being values, the general local scoping allows for veiling and defendin=
g I believe..<br><br></div><div class=3D"gmail_extra">I haven&#39;t quite g=
otten to factories yet, but my theory is that the holes in a factory, are q=
uite reminiscent of what 1ml calls &#39;large types&#39;, and so by bringin=
g together two large types, or opaque types, together with a translucent in=
terface to the type, through currying...<br></div><div class=3D"gmail_extra=
">Not quite there yet honestly, the basic file metaphor of source files mak=
es it a bit odd to express disjoint environments, without separate compilat=
ion.<br><br></div><div class=3D"gmail_extra">and FWIW, the descrim type and=
 the descrim key from keykos don&#39;t really match up, it seems like the k=
eykos descrim implemented in this descrim<br></div><div class=3D"gmail_extr=
a">would be something that if it type checks returns true (not particularly=
 more useful than just a normal type annotation)<br></div></div>

--001a11c2eb5aed7cd60529bbd02d--

--===============4143957067158934932==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk

--===============4143957067158934932==--