caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Yutaka OIWA <oiwa@yl.is.s.u-tokyo.ac.jp>
To: Vitaly Lugovsky <vsl@ontil.ihep.su>
Cc: J Farrand <farrand@cs.bris.ac.uk>, David Frese <dfrese@dfrese.de>,
	SooHyoung Oh <shoh@duonix.com>, Caml-list <caml-list@inria.fr>
Subject: Re: [Caml-list] Q: safe language
Date: 31 Aug 2002 01:03:15 +0900	[thread overview]
Message-ID: <vfi4rdc5o70.fsf@tuba.is.s.u-tokyo.ac.jp> (raw)
In-Reply-To: Vitaly Lugovsky's message of "Fri, 30 Aug 2002 18:26:07 +0400 (MSD)"

What a hot topic for me! :-)

>> On Fri, 30 Aug 2002 18:26:07 +0400 (MSD), Vitaly Lugovsky <vsl@ontil.ihep.su> said:

Vitaly> On Fri, 30 Aug 2002, J Farrand wrote:

Vitaly>  Ok, fixed. But I don't see any difference between segfault and NIL passed
Vitaly> as file descriptor. Program fails - and it does not matter, was it "low 
Vitaly> level" fault or unhandled exception or uncorrect behaviour.

No. SIGSEGV?  You are lucky.

You got SIGSEGV because an invalid pointer luckily points to the
outside of the process boundary. If it points to the inside of the
process, anything can be occur.  SIGSEGV, Malicious code injection,
clearing all your files, formatting your harddisk if you are a root,
and whatever else.

# SIGSEGV can be thought to be "safe" or "handled" if it is
# caused strictly by dereferencing "NULL" (or zero) in Unix environment.
# But many SIGSEGV are caused by buffer-overrun, dangling pointers, etc.
# Those are not safely handled.

The LISP exception you called it "unhandled" is actually handled.
It halts the program execution without relying to any luck.
It is defined to be so.

>> So for
>> example, C is not safe because you can derefence a bad pointer etc. and
>> cause a seg fault.

Vitaly>  Run C in a bytecode "safe" environment (there are some C implementations
Vitaly> with this functionality) - and it will become a "safe language"?

Yes.

If there is no free(), no pointer arithmetic, no casting, no buffer overflow,
it is OK.
Malloc-free problem can be solved by GC.
Buffer overflow?  Check the boundary like Java.
Pointer arithmetics?  Use fat pointers.
Pointer cast (to/from void*)?  Hmm... but it can be done.

I and many other people are working on this problem.


But, we must be aware, if we say "C language is not safe", or
"Scheme is type-safe", we assume some "normal" implementation
of the language.  If we pass "-unsafe" option to ocamlc, it becomes
unsafe.  A mini-Scheme compilers which Junior students in our
department wrote as an assignment does not check '() in cdr function and 
thus not type safe.  If you use our "Fail-Safe ANSI-C compiler"
(sorry not yet finished), C language becomes type-safe.
But you expected those tricky answers?  I think you don't.

# In addition, "safety" depends on its definition.
# If we assume a machine language which has only the type "word",
# and assume every machine state is "OK", then the machine language is
# "type-safe". But this is also not what we want.
# We must share some "normal" interpretation of the "safe" or
# "type-safe" states.

Vitaly>  And C runtime environment can have a well defined behaviour of what to do 
Vitaly> with wrong pointers.

In usual way of compilation, it is not possible. It requires
some heavy changing of the way of compilation, which most people
think "unusual".

-- 
Yutaka Oiwa              Yonezawa Lab., Dept. of Computer Science,
      Graduate School of Information Sci. & Tech., Univ. of Tokyo.
      <oiwa@yl.is.s.u-tokyo.ac.jp>, <yutaka@oiwa.shibuya.tokyo.jp>
PGP fingerprint = C9 8D 5C B8 86 ED D8 07  EA 59 34 D8 F4 65 53 61
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners


  parent reply	other threads:[~2002-08-30 16:13 UTC|newest]

Thread overview: 21+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2002-08-30  1:36 SooHyoung Oh
2002-08-30  8:41 ` sebastien FURIC
2002-08-30 12:44 ` Vitaly Lugovsky
2002-08-30 13:05   ` David Frese
2002-08-30 13:46     ` Oleg
2002-08-30 16:09       ` Yutaka OIWA
2002-08-30 13:49     ` Vitaly Lugovsky
2002-08-30 14:04       ` J Farrand
2002-08-30 14:26         ` Vitaly Lugovsky
2002-08-30 14:48           ` Nicolas Cannasse
2002-08-30 15:31             ` Vitaly Lugovsky
2002-08-30 14:55           ` Mike Lin
2002-08-30 14:58             ` Eric Newhuis
2002-08-30 16:03           ` Yutaka OIWA [this message]
2002-08-30 21:44           ` Oliver Bandel
2002-09-01  8:07         ` John Max Skaller
2002-08-30 14:50       ` David Frese
2002-08-30 15:38         ` Vitaly Lugovsky
2002-08-30 15:28     ` didier plaindoux
2002-08-30 14:41 ` Florian Hars
2002-08-30 14:42 ` Nicolas Cannasse

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=vfi4rdc5o70.fsf@tuba.is.s.u-tokyo.ac.jp \
    --to=oiwa@yl.is.s.u-tokyo.ac.jp \
    --cc=caml-list@inria.fr \
    --cc=dfrese@dfrese.de \
    --cc=farrand@cs.bris.ac.uk \
    --cc=shoh@duonix.com \
    --cc=vsl@ontil.ihep.su \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).