Designing a practical "safe C"

[Dan-164]

Here are some thoughts on the desirable
characteristics of a practical "safe C":

1) Usable whereever C is used (e.g. OS kernels,
embedded systems). This implies no built-in garbage
collection. The garbage collectors used with C/C++
could optionally be used, of course.

2) Standard C programs should compile without
modification (of course without modification there
would be no safety improvement).

3) "Safe C" code must interoperate seamlessly with
existing C/assembly code.

4) The language should try to facilitate safety, but
not attempt to absolutely guarantee it. Safety should
not be an all-or-nothing proposition.

5) Implied by the above, all manner of unsafe things
should be permitted by default.

6) The language should be as simple as possible.

I believe such an approach is the only one that would
appeal to current major users of C, because it allows
safety to be added incrementally to legacy code.

What about implementation?

Bounded pointers are great. Fat pointers, not so much.
It's more practical to simply declare that any pointer
arithmatic is unsafe. That's how C# works - that
language has (unsafe) pointer arithmatic without fat
pointers.

Null pointer dereferences are almost a non-issue
because 99% of the time the hardware will catch it (on
machines with MMUs). Not worth complicating the
language.

References are good. They reduce the need to take the
address of a local.

Hmm, what else? Actually, that might be a good place
to stop - just add bounded pointers and references to
C, and you've got quite a nice, practical language.
Maybe someone has already done it? Comments?

Dan



       
____________________________________________________________________________________
Be a better Globetrotter. Get better travel answers from someone who knows. Yahoo! Answers - Check it out.
http://answers.yahoo.com/dir/?link=list&sid=396545469

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[Michael Hicks]

Check out Deputy: http://deputy.cs.berkeley.edu/

-Mike

On Jun 19, 2007, at 11:43 PM, Dan wrote:

> Here are some thoughts on the desirable
> characteristics of a practical "safe C":
>
> 1) Usable whereever C is used (e.g. OS kernels,
> embedded systems). This implies no built-in garbage
> collection. The garbage collectors used with C/C++
> could optionally be used, of course.
>
> 2) Standard C programs should compile without
> modification (of course without modification there
> would be no safety improvement).
>
> 3) "Safe C" code must interoperate seamlessly with
> existing C/assembly code.
>
> 4) The language should try to facilitate safety, but
> not attempt to absolutely guarantee it. Safety should
> not be an all-or-nothing proposition.
>
> 5) Implied by the above, all manner of unsafe things
> should be permitted by default.
>
> 6) The language should be as simple as possible.
>
> I believe such an approach is the only one that would
> appeal to current major users of C, because it allows
> safety to be added incrementally to legacy code.
>
> What about implementation?
>
> Bounded pointers are great. Fat pointers, not so much.
> It's more practical to simply declare that any pointer
> arithmatic is unsafe. That's how C# works - that
> language has (unsafe) pointer arithmatic without fat
> pointers.
>
> Null pointer dereferences are almost a non-issue
> because 99% of the time the hardware will catch it (on
> machines with MMUs). Not worth complicating the
> language.
>
> References are good. They reduce the need to take the
> address of a local.
>
> Hmm, what else? Actually, that might be a good place
> to stop - just add bounded pointers and references to
> C, and you've got quite a nice, practical language.
> Maybe someone has already done it? Comments?
>
> Dan
>
>
>
>
> ______________________________________________________________________
> ______________
> Be a better Globetrotter. Get better travel answers from someone  
> who knows. Yahoo! Answers - Check it out.
> http://answers.yahoo.com/dir/?link=list&sid=396545469
>
> --
> cyclone-l mailing list  ::  cyclone-l@...
> https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[Greg Morrisett]

Dan wrote:
 > Here are some thoughts on the desirable
 > characteristics of a practical "safe C":
 >
 > 1) Usable whereever C is used (e.g. OS kernels,
 > embedded systems). This implies no built-in garbage
 > collection. The garbage collectors used with C/C++
 > could optionally be used, of course.
 >
 > 2) Standard C programs should compile without
 > modification (of course without modification there
 > would be no safety improvement).
 >
 > 3) "Safe C" code must interoperate seamlessly with
 > existing C/assembly code.
 >
 > 4) The language should try to facilitate safety, but
 > not attempt to absolutely guarantee it. Safety should
 > not be an all-or-nothing proposition.
 >
 > 5) Implied by the above, all manner of unsafe things
 > should be permitted by default.
 >

How about lint, SPLint, or even gcc -Wall?  :-)

Seriously, I've been thinking about doing something like
what you describe as a stripped down version of
Cyclone (code named Tempest.)  I might add polymorphism
and tagged unions to the list of things that I think
you can't really do without and have a truly safe subset.

I agree that references hit the sort of 90% mark for
stack-allocation (when compared to the complicated
region system of Cyclone.)

-Greg

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[Dan-164]

--- Greg Morrisett <greg@...> wrote:

> I agree that references hit the sort of 90% mark for
> stack-allocation (when compared to the complicated
> region system of Cyclone.)

A complementary feature would be a 'non-stack' pointer
type which is bounds checked to verify that it doesn't
point into the stack. If you declare all non-local
pointers to be of non-stack type, then stack safety
would be guaranteed (at the price of potentially
forcing more dynamic memory allocation than would
otherwise be required).

Dan



 
____________________________________________________________________________________
Looking for earth-friendly autos?
Browse Top Cars by "Green Rating" at Yahoo! Autos' Green Center.
http://autos.yahoo.com/green_center/

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[Geoffrey Alan Washburn]

Dan wrote:

Here are some thoughts on the desirable
characteristics of a practical "safe C":

1) Usable whereever C is used (e.g. OS kernels,
embedded systems). This implies no built-in garbage
collection. The garbage collectors used with C/C++
could optionally be used, of course.

2) Standard C programs should compile without
modification (of course without modification there
would be no safety improvement).

3) "Safe C" code must interoperate seamlessly with
existing C/assembly code.

4) The language should try to facilitate safety, but
not attempt to absolutely guarantee it. Safety should
not be an all-or-nothing proposition.

5) Implied by the above, all manner of unsafe things
should be permitted by default.

6) The language should be as simple as possible.
  

    Given all these competing requirements, I'm curious what notion of "safety" you could expect from such a language?  It sounds like what you really want is a static analysis tool for existing C programs (perhaps with annotations) instead of a new language. 



--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[LiteStar numnums]

Some parts of this message have been removed. Learn more about Nabble's security policy.

I'd have to agree with Mr. Washburn's points. Deputy should solve most of these issues, as well as static analysis tools for C. If you want the language to be 'as simple as possible', then why make a new language at all? We already have tools to do what this new language would do, so why do it at all?

On 6/20/07, Geoffrey Alan Washburn <geoffw@...> wrote:

Dan wrote:

Here are some thoughts on the desirable
characteristics of a practical "safe C":

1) Usable whereever C is used (e.g. OS kernels,
embedded systems). This implies no built-in garbage
collection. The garbage collectors used with C/C++

could optionally be used, of course.

2) Standard C programs should compile without
modification (of course without modification there
would be no safety improvement).

3) "Safe C" code must interoperate seamlessly with

existing C/assembly code.

4) The language should try to facilitate safety, but
not attempt to absolutely guarantee it. Safety should
not be an all-or-nothing proposition.

5) Implied by the above, all manner of unsafe things

should be permitted by default.

6) The language should be as simple as possible.
  

    Given all these competing requirements, I'm curious what notion of "safety" you could expect from such a language?  It sounds like what you really want is a static analysis tool for existing C programs (perhaps with annotations) instead of a new language. 

-- 
[Geoff Washburn|geoffw@...|
http://www.cis.upenn.edu/~geoffw/]

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

--
    "By cosmic rule, as day yields night, so winter summer, war peace, plenty famine. All things change. Air penetrates the lump of myrrh, until the joining bodies die and rise again in smoke called incense."

    "Men do not know how that which is drawn in different directions harmonises with itself. The harmonious structure of the world depends upon opposite tension like that of the bow and the lyre."

    "This universe, which is the same for all, has not been made by any god or man, but it always has been, is, and will be an ever-living fire, kindling itself by regular measures and going out by regular measures"
-- Heraclitus
--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[Dan-164]

--- LiteStar numnums <litestar@...> wrote:

> I'd have to agree with Mr. Washburn's points. Deputy
> should solve most of
> these issues, as well as static analysis tools for
> C. If you want the
> language to be 'as simple as possible', then why
> make a new language at all?
> We already have tools to do what this new language
> would do, so why do it at
> all?

Well, Deputy is a new language (or language extension
if you prefer) - and one that I was not aware of. It
is, indeed, close to what I had in mind.

So we're in violent agreement.

Dan



       
____________________________________________________________________________________
Need a vacation? Get great deals
to amazing places on Yahoo! Travel.
http://travel.yahoo.com/

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[Bob Paddock]

On Tuesday 19 June 2007 23:54, Michael Hicks wrote:
> Check out Deputy: http://deputy.cs.berkeley.edu/

http://research.microsoft.com/os/singularity/

"Singularity: Rethinking the Software Stack," among others.

--
                http://www.wearablesmartsensors.com/
 http://www.softwaresafety.net/ http://www.designer-iii.com/
                 http://www.unusualresearch.com/

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[John Regehr]

We've been using Deputy and it is nice.  The annotations started out being
a hassle but after using them for a little while I started to like them:
they force you to write down important properties of the code.  In a
parallel project we've been formally verifying some C code and in general
the Deputy annotation for a function is a subset of its actual
precondition.

The lack of a story for dyanmic allocation in Deputy is not so hot.  Even
on heapless embedded systems a stack reference that escapes into a global
or an ancestor stack frame pokes a hole in the safety model.

Null pointer story: on AVR, one of the embedded architectures we use, the
register file is mapped into low RAM.  So execute code such as "x->y=z"
when x is NULL and you are guaranteed to corrupt one or more registers if
the offset of field y is <32 (if >=32 you corrupt device registers instead
of CPU registers!).  Until you realize what is happening the resulting
program behavior just cannot be explained.

John


On Tue, 19 Jun 2007, Michael Hicks wrote:

> Check out Deputy: http://deputy.cs.berkeley.edu/
>
> -Mike
>
> On Jun 19, 2007, at 11:43 PM, Dan wrote:
>
> > Here are some thoughts on the desirable
> > characteristics of a practical "safe C":
> >
> > 1) Usable whereever C is used (e.g. OS kernels,
> > embedded systems). This implies no built-in garbage
> > collection. The garbage collectors used with C/C++
> > could optionally be used, of course.
> >
> > 2) Standard C programs should compile without
> > modification (of course without modification there
> > would be no safety improvement).
> >
> > 3) "Safe C" code must interoperate seamlessly with
> > existing C/assembly code.
> >
> > 4) The language should try to facilitate safety, but
> > not attempt to absolutely guarantee it. Safety should
> > not be an all-or-nothing proposition.
> >
> > 5) Implied by the above, all manner of unsafe things
> > should be permitted by default.
> >
> > 6) The language should be as simple as possible.
> >
> > I believe such an approach is the only one that would
> > appeal to current major users of C, because it allows
> > safety to be added incrementally to legacy code.
> >
> > What about implementation?
> >
> > Bounded pointers are great. Fat pointers, not so much.
> > It's more practical to simply declare that any pointer
> > arithmatic is unsafe. That's how C# works - that
> > language has (unsafe) pointer arithmatic without fat
> > pointers.
> >
> > Null pointer dereferences are almost a non-issue
> > because 99% of the time the hardware will catch it (on
> > machines with MMUs). Not worth complicating the
> > language.
> >
> > References are good. They reduce the need to take the
> > address of a local.
> >
> > Hmm, what else? Actually, that might be a good place
> > to stop - just add bounded pointers and references to
> > C, and you've got quite a nice, practical language.
> > Maybe someone has already done it? Comments?
> >
> > Dan
> >
> >
> >
> >
> > ______________________________________________________________________
> > ______________
> > Be a better Globetrotter. Get better travel answers from someone  
> > who knows. Yahoo! Answers - Check it out.
> > http://answers.yahoo.com/dir/?link=list&sid=396545469
> >
> > --
> > cyclone-l mailing list  ::  cyclone-l@...
> > https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l
>
>
> --
> cyclone-l mailing list  ::  cyclone-l@...
> https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l
>

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[Marius Nita-2]

An annotation-aided analysis for C is essentially a new C-like
programming language designed for minimum effort when porting C programs
to it. I suppose one can even think of Cyclone as an annotation-aided
analysis for C programs, with a very rich annotation language.

-marius

Geoffrey Alan Washburn wrote:

> Dan wrote:
>> Here are some thoughts on the desirable
>> characteristics of a practical "safe C":
>>
>> 1) Usable whereever C is used (e.g. OS kernels,
>> embedded systems). This implies no built-in garbage
>> collection. The garbage collectors used with C/C++
>> could optionally be used, of course.
>>
>> 2) Standard C programs should compile without
>> modification (of course without modification there
>> would be no safety improvement).
>>
>> 3) "Safe C" code must interoperate seamlessly with
>> existing C/assembly code.
>>
>> 4) The language should try to facilitate safety, but
>> not attempt to absolutely guarantee it. Safety should
>> not be an all-or-nothing proposition.
>>
>> 5) Implied by the above, all manner of unsafe things
>> should be permitted by default.
>>
>> 6) The language should be as simple as possible.
>>  
>
>     Given all these competing requirements, I'm curious what notion of
> "safety" you could expect from such a language?  It sounds like what you
> really want is a static analysis tool for existing C programs (perhaps
> with annotations) instead of a new language.
>
>
> --
> [Geoff Washburn|geoffw@...|http://www.cis.upenn.edu/~geoffw/]
>

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[John Regehr]

> to it. I suppose one can even think of Cyclone as an annotation-aided
> analysis for C programs, with a very rich annotation language.

C is annotation-aided assembly...

John

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[Geoffrey Alan Washburn]

Marius Nita wrote:

An annotation-aided analysis for C is essentially a new C-like programming language designed for minimum effort when porting C programs to it. I suppose one can even think of Cyclone as an annotation-aided analysis for C programs, with a very rich annotation language.

       I expect it is possible to debate the definitions, but I think saying that Cyclone is "C with annotations" is a bit of a stretch.  When I said "existing C programs (perhaps with annotations)", I meant valid inputs to a normal C compiler that could contain hints to the analysis tool within comments.  It has been a while since I've looked at a paper on Cyclone, but I will conjecture that not all of  the "annotations" in a Cyclone program are macro-expressible in such a way that there is a straightforward notion of "erasure" that gives you a grammatically valid C program.


--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l

[Greg Morrisett]

Geoffrey Alan Washburn wrote:
>       I expect it is possible to debate the definitions, but I think
> saying that Cyclone is "C with annotations" is a bit of a stretch.  When
> I said "existing C programs (perhaps with annotations)", I meant valid
> inputs to a normal C compiler that could contain hints to the analysis
> tool within comments.  It has been a while since I've looked at a paper
> on Cyclone, but I will conjecture that not all of  the "annotations" in
> a Cyclone program are macro-expressible in such a way that there is a
> straightforward notion of "erasure" that gives you a grammatically valid
> C program.

Very far from it indeed.  If you want the erasure property, then
I'd suggest looking at SPLint, Deputy, or commercial tools such as
Coverity's and Fortify's source code analyzers.  These tools don't
offer strong guarantees, but that's more or less impossible for C.

If you want something with stronger guarantees, then Ccured, D, and
Cyclone are reasonable things to study.  Ccured is much better
for adapting existing code.  In my opinion, Cyclone's a better
language for developing new systems code since it provides a lot of
features (e.g., tagged unions, datatypes, pattern matching,
exceptions, and polymorphism) that make it in essence a C-like
version of ML, but where allocation and storage lifetime is
made explicit and somewhat controllable.  Of course, if you want
those features and want to step outside the type system (e.g., to
do your own memory management), then it's relatively easy to
import and interoperate with C code.

-Greg

--
cyclone-l mailing list  ::  cyclone-l@...
https://lists.cs.cornell.edu/mailman/listinfo/cyclone-l