Re: [Haskell-cafe] US Homeland Security program language security risks

2008-01-09 Thread Yitzchak Gale
Galchin Vasili wrote on Friday, January 4:
  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.

Bulat Ziganshin wrote:
 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

Interestingly enough, a few days after this exchange, the
first public report was released from a large survey funded
by US Homeland Security on security of open source
projects. The survey was carried out by a company
called Coverity.

Among the projects making top grade for security - apparently
far better than most proprietary products, though complete
information about that is not public - were PHP, Perl, and
Python.

PHP? Come on, can't we do at least as well? But right now,
there is a technical impediment to the participation of
Haskell: the Coverity project currently only supports
projects written in C, C++, and Java. Haskell compilers
are often written in Haskell.

Any ideas? Perhaps Coverity's interest could be
piqued if they were made aware of Haskell's emergence
as an important platform in security-sensitive
industries such as finance and chip design, and of
the significant influence that Haskell is having on the
design of all other major programming languages.

The home page for the Coverity open source project
is at:

http://scan.coverity.com/

Some recent press coverage:

http://it.slashdot.org/article.pl?sid=08/01/09/0027229

http://www.zdnet.com.au/news/security/soa/11-open-source-projects-pass-security-health-check/0,130061744,339284949,00.htm

http://www.informationweek.com/story/showArticle.jhtml?articleID=205600229

-Yitz
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] US Homeland Security program language security risks

2008-01-09 Thread Bryan O'Sullivan
Yitzchak Gale wrote:

 Perhaps Coverity's interest could be
 piqued if they were made aware of Haskell's emergence
 as an important platform in security-sensitive
 industries such as finance and chip design, and of
 the significant influence that Haskell is having on the
 design of all other major programming languages.

During one of Simon PJ's tutorials at OSCON last year, a Coverity
engineer was in the audience.  He told us afterwards that he downloaded
the GHC source and gave a try at analysing it while Simon talked.  He
didn't get far, of course; their software wasn't built for the tricks
that -fvia-C plays.  But they have at least one person who was that
interested.

However, it would cost several million dollars to produce a tool as
slick as Coverity's for Haskell (Prevent is really very impressive).
That would rival Coverity's RD expenditure to date; they're a small
company.  I'd have a hard time believing that any such investment could
be recouped through commercial sales within the next decade.

b
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] US Homeland Security program language security risks

2008-01-09 Thread Isaac Dupree

Bryan O'Sullivan wrote:

Yitzchak Gale wrote:


Perhaps Coverity's interest could be
piqued if they were made aware of Haskell's emergence
as an important platform in security-sensitive
industries such as finance and chip design, and of
the significant influence that Haskell is having on the
design of all other major programming languages.


During one of Simon PJ's tutorials at OSCON last year, a Coverity
engineer was in the audience.  He told us afterwards that he downloaded
the GHC source and gave a try at analysing it while Simon talked.  He
didn't get far, of course; their software wasn't built for the tricks
that -fvia-C plays.  But they have at least one person who was that
interested.


unregisterised, it should be standard C without tricks, though still 
nothing like ordinary C and therefore possibly not analyzable


~Isaac
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] US Homeland Security program language security risks

2008-01-06 Thread Andrew Coppin

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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] US Homeland Security program language security risks

2008-01-06 Thread 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
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] US Homeland Security program language security risks

2008-01-06 Thread Daniel Fischer
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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] US Homeland Security program language security risks

2008-01-06 Thread 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] US Homeland Security program language security risks

2008-01-06 Thread 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] US Homeland Security program language security risks

2008-01-06 Thread Daniel Fischer
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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe