Steve Witham | 2 Jul 06:06 2009
Picon
Picon

A couple notes on Palm webOS security

These are from my ph file of random info, sorry for the format.
webOS apps are basically Javascript web pages running in a
specialized browser.

>Both Contacts and Calendar will allow applications to add
>information that will get merged into an integrated view.
>They don't allow applications to read, delete or update
>any data that wasn't created by the same application.

Reading between the lines it sounds like each app may have a
Linux user id.

>Note: Palm webOS applications are run from file:// URLs and thus aren't
>restricted by the single-origin policy that makes
>mixing services from different web sites difficult.

  --Steve
Rob Meijer | 2 Jul 09:40 2009
Picon
Picon

Re: A couple notes on Palm webOS security

On Thu, July 2, 2009 06:06, Steve Witham wrote:
> These are from my ph file of random info, sorry for the format.
> webOS apps are basically Javascript web pages running in a
> specialized browser.
>
>>Both Contacts and Calendar will allow applications to add
>>information that will get merged into an integrated view.
>>They don't allow applications to read, delete or update
>>any data that wasn't created by the same application.
>
> Reading between the lines it sounds like each app may have a
> Linux user id.

Possible, or alternatively a filesystem implementing a view based
access control mechanism. In MinorFs I use a similar mechanism, however
avoiding the per application view, and providing only a per non-persistent
process view and a per pseudo-persistent process view. The reason I
avoided implementing the per application view is that it is equivalent to
how languages like C++ provide the construct of static class level
variables, of what we know that it encourages the use of
undeniable/implicit authority
(that until recently I mistakingly used to call ambient authority, tnx
Mark/Alan). I have been arguing that providing a mechanism for
constructing undeniable/implicit authority in such a way, is a form of
hiding and dampening the problem of the single global namespace filesystem
access, while the pid and pppid approach, although a bigger leap for
architects and developers, does solve the problem in a structural way. I
argued that providing a mechanism for partially hiding the underlaying
problem may actually be harmful.

(Continue reading)

Matej Kosik | 2 Jul 14:03 2009
Picon

controversial article

Hello,

Most of us here are probably obsessed with something more or less
related to capabilities guarded:

1. either cryptographically
2. or by OS
3. or by the language.

Each kind is strong in different domain. All are important but I am
playing with the third kind.

Mark's thesis formulates the object-capability security model that is
supported by existing object-capability programming languages. Mark
thesis (as well as other texts) also defines the following concepts:
- defensive consistency
- defensive correctness

I hope that it is correct to say that all object-capability programming
languages can be used for creating software systems that are defensively
consistent but none of these languages (or platforms) can be used for
creating defensively correct software systems. (?)

What about defensive correctness?
Are there platforms that can be used for building defensively correct
software systems? (distributed or at least non-distributed).

I may be wrong but I assume that the answer is no. In my winter
experiments I was trying to figure out what is wrong with particular
object-capability programming language (Pict) that prevents me to use it
(Continue reading)

Trey Boudreau | 2 Jul 16:42 2009

Re: A couple notes on Palm webOS security

On Thu, Jul 02, 2009 at 12:06:32AM -0400, Steve Witham wrote:
> 
> These are from my ph file of random info, sorry for the format.
> webOS apps are basically Javascript web pages running in a
> specialized browser.
> 
> >Both Contacts and Calendar will allow applications to add
> >information that will get merged into an integrated view.
> >They don't allow applications to read, delete or update
> >any data that wasn't created by the same application.
> 
> Reading between the lines it sounds like each app may have a
> Linux user id.
> 
Android works this way.  Each app gets a unique user ID (and group ID, I
think).  Palm drew upon Google Android (and Apple iPhone) engineers when
staffing up for the Pre, so a user-per-app for webOS would have
precedence within the team.

-- Trey
Mark Miller | 2 Jul 19:59 2009
Picon

Re: controversial article

On Thu, Jul 2, 2009 at 5:03 AM, Matej Kosik <kosik-feEnI4mLD5ZfAtPiu00Fgw@public.gmane.org> wrote:


I hope that it is correct to say that all object-capability programming
languages can be used for creating software systems that are defensively
consistent but none of these languages (or platforms) can be used for
creating defensively correct software systems. (?)

AFAIK, that is true. I am not aware of any ocap *languages* that attempt to address this.

What about defensive correctness?
Are there platforms that can be used for building defensively correct
software systems? (distributed or at least non-distributed).

Non-distributed platforms, yes. All the members of the KeyKOS family (KeyKOS, EROS, GuardOS, CapROS, Coyotos) do/did a brilliant job at this.

Inherent in their approach, the kernel does no implicit allocation. All are based on rendezvous rather than asynchronous messages, and so no kernel buffering of messages is implied.

Distributed defensive correctness over unreliable networks is, almost by definition of "unreliable", impossible.

This suggests defining some possible approximations to defensive correctness:

* Distributed defensive correctness in the absence of spontaneous partitions or crashes, where "spontaneous" means, not caused by the actions of the programs we are concerned with.

* Defensive correctness up to resource exhaustion, which corresponds to the traditional concept of "liveness". Since this concept is well known in the literature, you may at least want to mention it, even if only to dismiss it.

* Budgeted and preemptively reclaimable resource allocation, in order to isolate the effects of resource exhaustion. For example, if we run a KeyKOS-like system but run only dynamically allocating languages -- or languages with no contract regarding resource use -- within each KeyKOS-like process, then an individual KeyKOS like process can still not be defensively correct, because we can't reason about if it will run out of storage while serving a valid request from a valid client. However, if it does, it only exhausts its own storage and thereby fails to service only its own clients. And it can't prevent the reclamation of its storage by an adequately authorized subject.
 
Hope this helps. Good luck!

--
Text by me above is hereby placed in the public domain

   Cheers,
   --MarkM

_______________________________________________
cap-talk mailing list
cap-talk@...
http://www.eros-os.org/mailman/listinfo/cap-talk
David Wagner | 2 Jul 21:17 2009
Picon

Re: controversial article

Matej Kosik  wrote:
>I hope that it is correct to say that all object-capability programming
>languages can be used for creating software systems that are defensively
>consistent but none of these languages (or platforms) can be used for
>creating defensively correct software systems. (?)

To be pedantic, they can plausibly be used to build defensively
correct software systems (they're Turing-complete, after all); it's
more that those languages don't provide special support for reasoning
about or ensuring defensive correctness.  So those languages don't
provide any extra help; if you want defensive correctness, you're
on your own.
Mark Miller | 2 Jul 21:55 2009
Picon

Re: controversial article

On Thu, Jul 2, 2009 at 12:17 PM, David Wagner <daw-Sd3DkRwxp1uueSrTVlFI5A@public.gmane.org> wrote:

Matej Kosik  wrote:
>I hope that it is correct to say that all object-capability programming
>languages can be used for creating software systems that are defensively
>consistent but none of these languages (or platforms) can be used for
>creating defensively correct software systems. (?)

To be pedantic, they can plausibly be used to build defensively
correct software systems (they're Turing-complete, after all); it's
more that those languages don't provide special support for reasoning
about or ensuring defensive correctness.  So those languages don't
provide any extra help; if you want defensive correctness, you're
on your own.

To be meta-hyper-turbo-pedantic, I claim this is false. A program is correct only if it relies only on specified properties of its platform, and not on unspecified properties of its platform's implementation. The specified semantics of all these languages either
1) assumes away the possibility of memory exhaustion, in which case their specification is not implementable (or only implementable up to fail-stop, which is inadequate for progress guarantees), or
2) they allow an out of memory condition to occur any step of computation that may allocate memory, including function/method calls in languages that allow recursion.

In either case, even a program as simple as

    function main() { foo(); }
    function foo() { print("hello world"); }

as expressed in almost any language in use today cannot be said to correctly implement the spec "prints 'hello world'." The most that can be said is that it will either do so or it will run out of memory. In Fortran 4, Occam, or any of the bare handful of languages without recursion or implicit dynamic allocation, given an appropriate and realizable spec, we can at least say that the above program will either fail to load or correctly run to completion. In these languages, one can write programs that would be defensively correct *given* that they successfully load. This is another useful approximation of defensive correctness -- perhaps the closest practical one.

--
Text by me above is hereby placed in the public domain

   Cheers,
   --MarkM

_______________________________________________
cap-talk mailing list
cap-talk@...
http://www.eros-os.org/mailman/listinfo/cap-talk
Toby Murray | 2 Jul 22:07 2009
Picon
Picon

Re: controversial article

On Thu, 2009-07-02 at 14:03 +0200, Matej Kosik wrote:
> I hope that it is correct to say that all object-capability programming
> languages can be used for creating software systems that are defensively
> consistent but none of these languages (or platforms) can be used for
> creating defensively correct software systems. (?)

I think it's important to define carefully what is meant by a
defensively correct software system.

(I'm yet to read your paper but want to be clear about what we're
talking about here first. Expect comments on the paper tomorrow
sometime.)

The traditional definitions of defensive correctness and consistency (if
I remember right) are framed in terms of servers and clients. A server
is defensively consistent if none of its clients can cause it to provide
incorrect service to any other client. A service is defensively correct
if it is defensively consistent and none of its clients can prevent it 
from giving correct service to any other.

With these definitions, suppose I implement a server in E whose clients
communicate with it from separate vats. Then I'd argue that it is quite
possible that this server could be defensively correct. In particular,
if the server is Functionally Pure, I fail to see how it cannot be
defensively correct.

If the clients are part of the same vat, then I'd argue that yes there
is no way to ensure defensive correctness (one client can always exhaust
all of the available memory or enter an infinite loop or whatever).

I had thought that the point of E was to allow one to ensure defensive
correctness between vats (although not within vats).

Cheers

Toby
Mark Miller | 2 Jul 22:21 2009
Picon

Re: controversial article

On Thu, Jul 2, 2009 at 1:07 PM, Toby Murray <toby.murray-wzN9gXeOksgSiZgQ0OGTRA@public.gmane.org> wrote:

 
I had thought that the point of E was to allow one to ensure defensive
correctness between vats (although not within vats).

Not "ensure", but to defend to an often practical degree. The approximations to defensive correctness I enumerated earlier in this thread derive from thinking about such practical defenses.

My section 5.7 "A Practical Standard for Defensive Programming" includes:

Defensive progress up to resource exhaustion, where we include non-termination,
such as an infinite loop, as a form of resource exhaustion. Protocols that achieve
only defensive progress up to resource exhaustion are normally regarded as satisfying
a meaningful liveness requirement. Whether this standard is usefully stricter than
cooperative progress we leave to the judgement of the reader.

While it is true that the infinite loop example only applies within a vat, E's distributed semantics require unbounded message buffering in the same sense in which its local semantics requires unbounded heap and stack. Unbounded buffering requirements do not normally prevent a protocol from claiming "liveness", FWIW.

--
Text by me above is hereby placed in the public domain

   Cheers,
   --MarkM

_______________________________________________
cap-talk mailing list
cap-talk@...
http://www.eros-os.org/mailman/listinfo/cap-talk
Karp, Alan H | 2 Jul 22:40 2009
Picon

Re: controversial article

MarkM wrote:

 

While it is true that the infinite loop example only applies within a vat, E's distributed semantics require unbounded message buffering in the same sense in which its local semantics requires unbounded heap and stack. Unbounded buffering requirements do not normally prevent a protocol from claiming "liveness", FWIW.

Does that mean buffering on the sender side is better for defensive correctness?

________________________

Alan Karp

Principal Scientist

Virus Safe Computing Initiative

Hewlett-Packard Laboratories

1501 Page Mill Road

Palo Alto, CA 94304

(650) 857-3967, fax (650) 857-7029

http://www.hpl.hp.com/personal/Alan_Karp

 

_______________________________________________
cap-talk mailing list
cap-talk@...
http://www.eros-os.org/mailman/listinfo/cap-talk

Gmane