Re: Methodenstreit? (was:Re: off topic - Freud und so <g>)

[ralf.stephan@fitug.de]

mel:
> Quoting ralf.stephan@fitug.de (ralf.stephan@fitug.de):
> > mel über Psychologie:
> > > Das ist anders bei einem OS wie Linux (das war der Kontext - deswegen
> > > "technisch"). Da kann man z.B. eine Menge messen oder mit Konzepten 
> > > vergleichen. Hej, wenn Du ganz verrueckt bist, kannst Du das sogar
> > > formal modelieren und Beweise fuehren! Dazu gibt es wunderschoene
> > > Theorien, die nur deswegen nicht eingesetzt werden, weil komischerweise
> > > keiner der Programmierer Lust hat, in einer Syntax, bei der der Formel-
> > > editor Schluckauf bekommt, 10 Seiten lang zu beweisen, dass ein paar 
> > 
> > Nein.  Solche Beweise lassen sich inzwischen automatisieren, aber
> 
> ja? Tun sie das? AFAIK nicht (nur ganz kleine Teilmengen der Beweise
> lassen sich automatisieren) und meist sind diese automatischen Systeme
> nach wie vor ziemlich manuell (also nur als Unterstuetzung gedacht).
> Wenn ich mich da irre, dann such mir doch bitte die Referenz raus,
> das interessiert mich wirklich.

Ging doch schneller.  Du irrst Dich nicht insofern, als sich nur
bestimmte Beweise automatisieren lassen.  Habe aber auch nicht 'alle'
geschrieben ;)  Alles weitere von mir war handwaving.  Hier die Ref.,
die auch sonst recht interessant ist, beurteile selbst die Glaubwürde:

http://www.jya.com/subversion.htm
(Subversion: The Neglected Aspect of Computer Security)

   Harrison, Ruzzo, and Ullman in their paper "Protection in Operating
   Systems" [4] provide conclusive proof that there is no algorithm that
   can prove an arbitrary protection system (such as an operating system)
   safe. This means it cannot be proven that an arbitrary operating
   system can withhold unauthorized information from malicious users.
   This is because a system may not be (and usually is not) designed in a
   manner that its safety can be precisely determined. However, for a
   properly designed system the safety question could be decided. But,
   the constraints placed on these "model" systems are too severe to
   prove practical for the evaluation of current operating systems. In
   particular, systems designed using the security kernel technology [3]
   can be definitively evaluated for security. This technology will be
   briefly discussed in Chapter V.


ralf
-- 
http://www.tmt.de/~stephan/