US Homeland Security program language security risks

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
24 messages Options
12
Reply | Threaded
Open this post in threaded view
|

US Homeland Security program language security risks

Vasili I. Galchin
Hello,
 
 
I stumbled across this page. It seems that Haskell and other strongly typed functional languages like Ml/OCaml will fare much, much better, e.g. buffer overrun. Thoughts . .... comments.
 
Vasili    

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Bulat Ziganshin-2
Hello Galchin,

Friday, January 4, 2008, 12:36:03 AM, you wrote:

>  I stumbled across this page. It seems that Haskell and other
> strongly typed functional languages like Ml/OCaml will fare much,
> much better, e.g. buffer overrun. Thoughts . .... comments.

for me, it looks like saying that haskell better uses CPU registers :)
the truth is that modern languages (including Java/C#) doesn't use
buffers directly. i don't have experience of their usage, but for
Haskell i had memory referencing problems only when using unsafe*
tricks

--
Best regards,
 Bulat                            mailto:[hidden email]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Andrew Coppin
In reply to this post by Vasili I. Galchin
Galchin Vasili wrote:
> Hello,
>  
> https://buildsecurityin.us-cert.gov/daisy/bsi/articles/knowledge/coding/295.html
>  
> I stumbled across this page. It seems that Haskell and other strongly
> typed functional languages like Ml/OCaml will fare much, much better,
> e.g. buffer overrun. Thoughts . .... comments.

Human kind has yet to design a programming language which eliminates all
possible bugs. ;-)

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Mads Lindstrøm
Hi,

Andrew Coppin wrote:

> Galchin Vasili wrote:
> > Hello,
> >  
> > https://buildsecurityin.us-cert.gov/daisy/bsi/articles/knowledge/coding/295.html
> >  
> > I stumbled across this page. It seems that Haskell and other strongly
> > typed functional languages like Ml/OCaml will fare much, much better,
> > e.g. buffer overrun. Thoughts . .... comments.
>
> Human kind has yet to design a programming language which eliminates all
> possible bugs. ;-)
And we never will. See http://en.wikipedia.org/wiki/Halting_problem .


Greetings,

Mads

>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Andrew Coppin
Mads Lindstrøm wrote:
> Hi,
>
> Andrew Coppin wrote:
>  
>> Human kind has yet to design a programming language which eliminates all
>> possible bugs. ;-)
>>    
> And we never will.

Quite so. How can a machine possibly tell whether a given behaviour is a
"bug" or an "intended behaviour"? This is impossible. ;-)

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Daniel Fischer-4
In reply to this post by Mads Lindstrøm
Am Sonntag, 6. Januar 2008 14:27 schrieb Mads Lindstrøm:

> Hi,
>
> Andrew Coppin wrote:
> > Galchin Vasili wrote:
> > > Hello,
> > >
> > > https://buildsecurityin.us-cert.gov/daisy/bsi/articles/knowledge/coding
> > >/295.html
> > >
> > > I stumbled across this page. It seems that Haskell and other strongly
> > > typed functional languages like Ml/OCaml will fare much, much better,
> > > e.g. buffer overrun. Thoughts . .... comments.
> >
> > Human kind has yet to design a programming language which eliminates all
> > possible bugs. ;-)
>
> And we never will. See http://en.wikipedia.org/wiki/Halting_problem .
>
>
> Greetings,
>
> Mads
>

Just because I don't know:
what bugs would be possible in a language having only the instruction
return ()
(';' for imperative programmers)?
Cheers,
Daniel
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Andrew Coppin
Daniel Fischer wrote:
> Just because I don't know:
> what bugs would be possible in a language having only the instruction
> return ()
>  

Bug #1: You cannot write any nontrivial programs. ;-)

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Achim Schneider
In reply to this post by Daniel Fischer-4
Daniel Fischer <[hidden email]> wrote:

> Just because I don't know:
> what bugs would be possible in a language having only the instruction
> return ()
> (';' for imperative programmers)?
>
/me waves meaningful with his hand.

--
(c) this sig last receiving data processing entity. Inspect headers for
past copyright information. All rights reserved. Unauthorised copying,
hiring, renting, public performance and/or broadcasting of this
signature prohibited.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Daniel Fischer-4
In reply to this post by Andrew Coppin
Am Sonntag, 6. Januar 2008 15:18 schrieb Andrew Coppin:
> Daniel Fischer wrote:
> > Just because I don't know:
> > what bugs would be possible in a language having only the instruction
> > return ()
>
> Bug #1: You cannot write any nontrivial programs. ;-)
>
That's not a bug, that's a feature.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Peter Hercek-2
In reply to this post by Mads Lindstrøm
Mads Lindstrøm wrote:
> Andrew Coppin wrote:
>> Human kind has yet to design a programming language which eliminates all
>> possible bugs. ;-)
> And we never will. See http://en.wikipedia.org/wiki/Halting_problem .

If you limit usage of general recursion (and rather favor structural
  recursion) then you can mitigate the halting problem.
But there always will be specification bugs (when one implenetes
something else than what was needed).

Peter.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program blahBlah...

jerzy.karczmarczuk
Peter Hercek writes:
>> Andrew Coppin wrote:

>>> Human kind has yet to design a programming language which eliminates all
>>> possible bugs. ;-)
> ...you can mitigate the halting problem.
> But there always will be specification bugs (when one implenetes something
> else than what was needed).

Look, you are descending an infinite ramp to conceptual hell, the hell of
triviality. Now, you will discuss "what is needed", and from FP we get into
politics!

But, if it is something you need...

Read then the passage of "Earthsea" of Ursula LeGuin. There is something
about a language in which YOU COULD NOT LIE. It was the ancient tongue of
dragons.

Now we see why the dragons are extinct...
They were incompatible with the Democracy, AND with Computing Technology...

Jerzy Karczmarczuk

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Achim Schneider
In reply to this post by Daniel Fischer-4
Daniel Fischer <[hidden email]> wrote:

> Am Sonntag, 6. Januar 2008 15:18 schrieb Andrew Coppin:
> > Daniel Fischer wrote:
> > > Just because I don't know:
> > > what bugs would be possible in a language having only the
> > > instruction return ()
> >
> > Bug #1: You cannot write any nontrivial programs. ;-)
> >
> That's not a bug, that's a feature.
>
That's an interesting task: Design a non-touring complete,
restricted language in which every expression is decidable, without
making the language unusable for usual programming problems.

--
(c) this sig last receiving data processing entity. Inspect headers for
past copyright information. All rights reserved. Unauthorised copying,
hiring, renting, public performance and/or broadcasting of this
signature prohibited.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: US Homeland Security program language security risks

Heinrich Apfelmus
Achim Schneider wrote:
> That's an interesting task: Design a non-touring complete,
> restricted language in which every expression is decidable, without
> making the language unusable for usual programming problems.

Have a look about dependently typed languages like Epigram:

   http://www.e-pig.org/


Regards,
apfelmus

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: US Homeland Security program language security risks

Daniel Fischer-4
In reply to this post by Achim Schneider
Am Sonntag, 6. Januar 2008 15:54 schrieb Achim Schneider:

> Daniel Fischer <[hidden email]> wrote:
> > Am Sonntag, 6. Januar 2008 15:18 schrieb Andrew Coppin:
> > > Daniel Fischer wrote:
> > > > Just because I don't know:
> > > > what bugs would be possible in a language having only the
> > > > instruction return ()
> > >
> > > Bug #1: You cannot write any nontrivial programs. ;-)
> >
> > That's not a bug, that's a feature.
>
> That's an interesting task: Design a non-touring complete,
> restricted language in which every expression is decidable, without
> making the language unusable for usual programming problems.

I'm not a logician, but didn't Gödel prove that you couldn't express the
(full) arithmetic of natural numbers in such a language?
Of course it might be possible to express a sufficiently interesting part of
it, but I should be surprised.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: US Homeland Security program language security risks

Derek Elkins
On Sun, 2008-01-06 at 16:19 +0100, Daniel Fischer wrote:

> Am Sonntag, 6. Januar 2008 15:54 schrieb Achim Schneider:
> > Daniel Fischer <[hidden email]> wrote:
> > > Am Sonntag, 6. Januar 2008 15:18 schrieb Andrew Coppin:
> > > > Daniel Fischer wrote:
> > > > > Just because I don't know:
> > > > > what bugs would be possible in a language having only the
> > > > > instruction return ()
> > > >
> > > > Bug #1: You cannot write any nontrivial programs. ;-)
> > >
> > > That's not a bug, that's a feature.
> >
> > That's an interesting task: Design a non-touring complete,
> > restricted language in which every expression is decidable, without
> > making the language unusable for usual programming problems.
>
> I'm not a logician, but didn't Gödel prove that you couldn't express the
> (full) arithmetic of natural numbers in such a language?
> Of course it might be possible to express a sufficiently interesting part of
> it, but I should be surprised.

What Goedel meant by "arithmetic" is a bit more than one usually
associates with the term.  One person mentioned Epigram.  Most theorem
provers and most? (of the few) dependently typed programming languages
would fit Achim's criterion depending on the range of "usable" and
"usual".  Coq, for example, is likely to be capable of formalizing just
about anything you'd want.  Of course, there is one class of
"programming problem" that we can already say can't be handled; namely
implementing interpreters (for Turing complete languages).  We can
formalize analyses, make compilers, prove the compilers correct with
respect to a semantics, and even prove that a -description- of an
interpreter correctly implements the semantics, but we can't actually
-run- the interpreter.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: US Homeland Security program language security risks

Cristian Baboi
In reply to this post by Daniel Fischer-4
On Sun, 06 Jan 2008 17:19:31 +0200, Daniel Fischer  
<[hidden email]> wrote:

> Am Sonntag, 6. Januar 2008 15:54 schrieb Achim Schneider:
>> Daniel Fischer <[hidden email]> wrote:
>> > Am Sonntag, 6. Januar 2008 15:18 schrieb Andrew Coppin:
>> > > Daniel Fischer wrote:
>> > > > Just because I don't know:
>> > > > what bugs would be possible in a language having only the
>> > > > instruction return ()
>> > >
>> > > Bug #1: You cannot write any nontrivial programs. ;-)
>> >
>> > That's not a bug, that's a feature.
>>
>> That's an interesting task: Design a non-touring complete,
>> restricted language in which every expression is decidable, without
>> making the language unusable for usual programming problems.

> I'm not a logician, but didn't Gödel prove that you couldn't express the
> (full) arithmetic of natural numbers in such a language?
> Of course it might be possible to express a sufficiently interesting  
> part of
> it, but I should be surprised.

Neither do I, but if you have non turing algorithms, maybe you could do it.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: US Homeland Security program language security risks

Gwern Branwen
In reply to this post by Achim Schneider
On 2008.01.06 15:54:00 +0100, Achim Schneider <[hidden email]> scribbled 0.6K characters:

> Daniel Fischer <[hidden email]> wrote:
>
> > Am Sonntag, 6. Januar 2008 15:18 schrieb Andrew Coppin:
> > > Daniel Fischer wrote:
> > > > Just because I don't know:
> > > > what bugs would be possible in a language having only the
> > > > instruction return ()
> > >
> > > Bug #1: You cannot write any nontrivial programs. ;-)
> > >
> > That's not a bug, that's a feature.
> >
> That's an interesting task: Design a non-touring complete,
> restricted language in which every expression is decidable, without
> making the language unusable for usual programming problems.
Total functional programming, yay: <http://lambda-the-ultimate.org/node/2003>.

--
gwern
$ Majic shaped Grove infrastructure Spoke BOSS mercur SEIDM BX

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

attachment0 (196 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Re: US Homeland Security program language security risks

MigMit
In reply to this post by Achim Schneider
> That's an interesting task: Design a non-touring complete,
> restricted language in which every expression is decidable, without
> making the language unusable for usual programming problems.

Well, I did something like that a few years ago - it was a sort of  
assembler language, allowing the programmer to, say, sort an array,  
but not to calculate Akkerman function.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: US Homeland Security program language security risks

Ben Franksen
Miguel Mitrofanov wrote:
>> That's an interesting task: Design a non-touring complete,
>> restricted language in which every expression is decidable, without
>> making the language unusable for usual programming problems.
>
> Well, I did something like that a few years ago - it was a sort of
> assembler language, allowing the programmer to, say, sort an array,
> but not to calculate Akkerman function.

P. Wadler, in his famous paper "Theorems for free!", writes on page
2: "Indeed, every recursive function that can be proved total in second
order Peano arithmetic can be written as a term in the Girard/Reynolds
calculus [...]. This includes, for instancs, Ackerman's function [...], but
excludes interpreters for most languages (including the Girard/Reynolds
calculus itself)." BTW, another name for the Girard/Reynolds calculus
is "(pure) polymorphic lambda calculus"; and yes, it is strongly
normalizing. (Wadler cites some papers to support the above claim.)

It seems there is quite a lot of interesting stuff that can be done in a
language where every expression is guaranteed to terminate.

Cheers
Ben

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: US Homeland Security program language security risks

Wolfgang Jeltsch-2
In reply to this post by MigMit
Am Sonntag, 6. Januar 2008 20:04 schrieb Miguel Mitrofanov:
> > That's an interesting task: Design a non-touring complete,
> > restricted language in which every expression is decidable, without
> > making the language unusable for usual programming problems.
>
> Well, I did something like that a few years ago - it was a sort of
> assembler language, allowing the programmer to, say, sort an array,
> but not to calculate Akkerman function.

Epigram even allows you Ackermann’s function.

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12