Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.forth > #30977 > unrolled thread
| Started by | rickman <gnuarm@gmail.com> |
|---|---|
| First post | 2014-05-29 21:35 -0400 |
| Last post | 2014-07-17 16:09 -0400 |
| Articles | 20 on this page of 190 — 24 participants |
Back to article view | Back to comp.lang.forth
MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-29 21:35 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-29 19:09 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-29 19:13 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-29 23:00 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-29 20:25 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 20:23 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 22:15 -0700
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-05-30 15:13 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-30 13:51 -0400
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-05-30 21:08 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-30 12:22 -0700
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-05-30 21:41 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-30 13:28 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-30 17:55 -0400
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-30 16:29 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-30 14:18 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-30 18:07 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-30 17:24 -0700
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-02 11:10 +0200
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-02 10:57 +0000
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-02 13:34 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 20:10 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-29 20:29 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 21:02 -0700
Re: MSP430-Stamp "Rod Pemberton" <dont_use_email@xnothavet.cqm> - 2014-05-30 04:05 -0400
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-05-30 15:13 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 19:57 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-29 23:32 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 21:07 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-05-30 02:39 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-07-17 12:40 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-07-17 16:08 -0400
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-07-18 00:06 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-07-18 08:22 -0700
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-07-18 23:42 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-07-18 18:28 -0400
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-07-19 01:41 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-07-18 19:48 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-07-18 16:59 -0700
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-07-19 14:30 +0200
Re: MSP430-Stamp Gary Bergstrom <forthprgrmr@gmail.com> - 2014-07-19 08:23 -0700
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-07-21 10:42 +0200
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-05-30 03:03 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 07:47 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-31 11:36 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-31 09:34 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 10:09 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-31 10:52 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 01:28 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 22:41 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 02:00 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 23:07 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 03:13 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-01 07:15 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 12:33 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-01 09:45 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 13:10 -0400
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-06-01 18:38 +0200
Re: MSP430-Stamp babruehl@gmail.com - 2014-06-01 11:40 -0700
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-06-01 11:13 +0200
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-01 09:50 +0000
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-06-01 12:47 +0200
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-01 04:05 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 12:39 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-01 10:00 -0700
Re: MSP430-Stamp babruehl@gmail.com - 2014-06-01 11:45 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 14:57 -0400
Re: MSP430-Stamp "VisualForth.com" <babruehl@gmail.com> - 2014-06-01 12:01 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 15:12 -0400
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-05-30 03:12 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-30 14:02 -0400
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-05-31 03:33 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 07:19 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-31 12:01 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 09:15 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 13:51 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-05-31 14:20 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 14:51 -0700
Re: MSP430-Stamp "VisualForth.com" <babruehl@gmail.com> - 2014-05-31 16:22 -0700
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-01 01:33 +0200
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-05-31 17:31 -1000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 21:48 -0700
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-05-31 19:12 -1000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 22:25 -0700
Re: MSP430-Stamp stephenXXX@mpeforth.com (Stephen Pelc) - 2014-06-01 09:45 +0000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-01 04:16 -0700
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-06-01 08:51 -1000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 21:03 -0700
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-01 21:17 +0200
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-04 22:46 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-05 13:27 +0000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-05 08:39 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-05 16:10 +0000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-05 11:10 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-05 19:52 +0000
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-05 23:25 +0200
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-05 15:02 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-06 10:56 +0000
Correct Software and Specifications (was Re: MSP430-Stamp) Paul E Bennett <Paul_E.Bennett@topmail.co.uk> - 2014-06-09 09:59 +0100
Re: MSP430-Stamp mhx@iae.nl - 2014-06-05 14:30 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-06 10:59 +0000
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-05 15:57 +0200
Formal specifications etc. (was: MSP430-Stamp) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2014-06-05 15:34 +0000
Re: Formal specifications etc. Paul Rubin <no.email@nospam.invalid> - 2014-06-05 11:48 -0700
Re: Formal specifications etc. anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2014-06-05 19:46 +0000
Re: Formal specifications etc. (was: MSP430-Stamp) Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-05 23:02 +0200
Re: Formal specifications etc. Paul Rubin <no.email@nospam.invalid> - 2014-06-05 14:15 -0700
Re: Formal specifications etc. rickman <gnuarm@gmail.com> - 2014-06-05 17:33 -0400
Re: Formal specifications etc. Paul Rubin <no.email@nospam.invalid> - 2014-06-05 15:32 -0700
Re: Formal specifications etc. Andrew Haley <andrew29@littlepinkcloud.invalid> - 2014-06-06 04:00 -0500
Re: Formal specifications etc. (was: MSP430-Stamp) albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-06 11:05 +0000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-05 11:01 -0700
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-06 01:09 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-05 22:01 -0400
Re: MSP430-Stamp stephenXXX@mpeforth.com (Stephen Pelc) - 2014-05-31 16:47 +0000
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-30 12:11 -0700
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-06 12:54 +0200
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-02 11:39 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-02 12:15 -0400
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-03 10:26 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-03 12:18 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-02 10:04 -0700
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-03 11:51 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-03 13:33 -0400
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-06 13:02 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-06 17:31 -0400
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-06-06 16:30 -1000
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-06 22:52 -0400
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-07 11:58 +0000
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-07 11:40 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-07 20:01 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-08 16:05 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-08 22:28 -0400
Re: MSP430-Stamp Gary Bergstrom <forthprgrmr@gmail.com> - 2014-06-08 20:36 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-08 21:38 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-09 14:36 -0400
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-09 02:45 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-09 03:18 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-09 15:57 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-08 16:20 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-03 20:42 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-03 21:05 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-04 10:43 +0000
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-03 21:28 -0700
Re: MSP430-Stamp "VisualForth.com" <babruehl@gmail.com> - 2014-06-03 22:43 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-03 23:31 -0700
Re: MSP430-Stamp "VisualForth.com" <babruehl@gmail.com> - 2014-06-04 04:13 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-03 01:41 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-03 01:51 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-03 16:19 +0100
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-03 09:14 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-03 13:19 -0400
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-06-03 07:43 -1000
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-03 20:56 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-04 10:51 +0000
Re: MSP430-Stamp VisualForth <babruehl@gmail.com> - 2014-06-04 04:06 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-06 21:26 -0400
Re: MSP430-Stamp "VisualForth.com" <babruehl@gmail.com> - 2014-06-06 20:40 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-07 03:18 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-07 04:35 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-07 12:01 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-09 03:47 -0700
Re: MSP430-Stamp Mikael Nordman <oh2aun@gmail.com> - 2014-06-09 09:28 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-11 07:35 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-11 10:43 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-11 15:52 -0700
Re: MSP430-Stamp Coos Haak <chforth@hccnet.nl> - 2014-06-12 02:06 +0200
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-06-11 15:13 -1000
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-12 02:16 -0700
Re: MSP430-Stamp Mikael Nordman <oh2aun@gmail.com> - 2014-06-11 12:56 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-09 16:46 -0400
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-09 03:49 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-09 09:47 -0700
Re: MSP430-Stamp Rikard Lang <rikard.lang@gmail.com> - 2014-06-09 23:16 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-10 07:48 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-11 07:23 -0700
Re: MSP430-Stamp David Schultz <abuse@127.0.0.1> - 2014-06-11 18:00 -0500
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-12 02:14 -0400
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-12 02:13 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-12 13:04 -0400
Re: MSP430-Stamp David Schultz <abuse@127.0.0.1> - 2014-06-12 18:06 -0500
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-12 19:29 -0400
Re: MSP430-Stamp David Schultz <abuse@127.0.0.1> - 2014-06-13 18:48 -0500
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-11 07:26 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-11 10:45 -0700
Re: MSP430-Stamp JUERGEN <epldfpga@aol.com> - 2014-06-13 00:03 -0700
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-18 11:11 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-18 05:27 -0400
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-18 12:29 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-07-17 16:09 -0400
Page 6 of 10 — ← Prev page 1 … 4 5 [6] 7 8 … 10 Next page →
| From | albert@spenarnc.xs4all.nl (Albert van der Horst) |
|---|---|
| Date | 2014-06-06 10:59 +0000 |
| Message-ID | <53919f0d$0$4852$e4fe514c@dreader35.news.xs4all.nl> |
| In reply to | #31224 |
In article <e1613a49-e9b7-4beb-9d6a-dc46b19f8fec@googlegroups.com>, <mhx@iae.nl> wrote: >On Thursday, June 5, 2014 2:27:47 PM UTC+1, Albert van der Horst wrote: >[..] >> Instead he ground through the >> electric cable. This worker was not grounded. > >Two wrongs making one lucky guy. If the cable would've carried the kV MA current that are customary with Hoogovens, a pair of rubber boots wouldn't have helped him. Fortunately the cable was still unpowered. > >-marcel > -- Albert van der Horst, UTRECHT,THE NETHERLANDS Economic growth -- being exponential -- ultimately falters. albert@spe&ar&c.xs4all.nl &=n http://home.hccnet.nl/a.w.m.van.der.horst
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2014-06-05 15:57 +0200 |
| Message-ID | <lmpt18$7k2$1@online.de> |
| In reply to | #31201 |
Paul Rubin wrote:
> Bernd Paysan <bernd.paysan@gmx.de> writes:
>>>> The amount of bugs in a reviewed and "debugged" code-base is roughly
>>>> the same per kLoC..
>>> What? No I don't believe that--for example TeX has had very few bugs
>>> reported in its entire history, while Linux has had hundreds.
>> TeX is an awfully small program by modern standards. ... Linux has
>> more than 10 million LoCs. You would expect it to have three orders
>> of magnitude more bugs than TeX. And indeed, it does. The big pile
>> of LaTeX extensions have a lot more bugs than TeX, the program.
>
> Hmm, yeah, that's true about TeX being relatively small but I still
> don't believe the bugs per kloc is similar, and your point about LaTeX
> corroborates that (less care was taken with the LaTeX extensions). I'd
> be interested in actual data. Particularly I haven't found the
> Altran/Praxis claims to be terribly implausible despite being a sales
> pitch:
>
> http://www.crosstalkonline.org/storage/issue-archives/2005/200512/200512-Croxford.pdf
> http://www.spectrum.ieee.org/sep05/1454
Yes, I like the six principles they use. The formal notation is only point
1; point 2 is using e.g. formal proofs to validate that the deliverable
meets the spec (you could also use some test driven design, that would cover
point 2 as well). The next points are very obviously what we Forthers do:
6. Do the hard thing first, with building prototypes and throwing things
that don't quite work away and redoing them, 5. design software that is easy
to validate (by factoring into small chunks that can be verified in
isolation), 4. Saying things only once - this is factoring, creating DSLs
that make it easy to formulate the actual problem in a compact, non-
redundant way, 3. Small, incremental development (add a word and run all the
testing stuff).
I'm mostly happy with this paper; I can recommend reading it and using that
approach. What I think can be done better is the specification stuff.
Actually the thinking that you should use a formal method to write down your
spec is *right*. Fundamentally *right*. That's not what I'm going to argue
about. The wrong here is that you have to write the formal spec, which is
actually a programming language of sorts (as it is formal and has a well-
defined semantics), and *then* have to write it again in another programming
language (the implementation language). Don't. Instead try to compile your
formal language; this is quite often possible, way more often than you think
(e.g. Verilog was originally designed as specification language to formally
verify hand-drawn circuits; but it soon was compiled instead). Or better:
Make a formal language that allows you to specify your problem easily, i.e.
a DSL.
The "say things only once" contradicts the formal spec. You should really
say things only once, and thus you must spend the effort (i.e. writing a
DSL) to be able to say things only once. The code you use to solve your
problem must be close to what you expect from a specification language.
The zero-defect example that they list in the end of the article is just
10kLoCs, and it was written quite fast (38LoCs/day is really fast). If you
want to deliver zero-defect products, you absolutely have to be small. And
of course you need a sound development approach that gets you a low
defect/kLoC rate. Because with the usual approach, you get out of the
defect-free zone at 1kLoC. 1kLoC is not enough.
>> People have analyzed security relevant programs in different programming
>> languages, and the number of security problems per amount of code was
>> about
>> equal. Java Programmers make different mistakes.
>
> 1. I don't think you can consider all "security problems" to be
> equivalent. Spilling keys is much worse than almost any protocol error!
Nope. Spilling keys is just as bad as e.g. not detecting a MITM attack.
With spilled keys, you can attack the connection as man in the middle. If
the code contains a bug that prevents detecting the MITM attack without the
attacker needing the key, the effect is the same. This sort of "goto
fail;"-Bug (we have seen them in almost all SSL implementations with the
Frankencert suite) is not crashing the program, it is not exposing any
memory or such.
The assumption that Java helps you to avoid crazy stuff IMHO is completely
unfounded. The actually only crashs in my Gforth Android app that Google
reported to me as ANR were in the few hundred lines of Java code, and they
were null pointer exceptions. I got null pointers I didn't expect I would
(nor does the spec of these callbacks say they could be null pointers, but
they were).
> 2. I think what may really be going on here is a kind of "risk
> thermostat" effect, where bugs decrease to a certain level because that
> level is tolerable to the development and release process, an issue
> orthogonal to the programming language. E.g. a typical internet shop
> will develop and test their code til it seems to work, then (if we're
> lucky) they release it to interested customers for beta test, collect
> further bug reports and fix those, and then when the bug reports slow
> down enough or stop, they release to production. Bugs are considered
> under control if enough less time is spent fixing them than implementing
> new features.
Maybe.
> For a lolcat app, that's not too bad a process. It's like making
> consumer electronics: if a DVD player basically works and doesn't break
> too easily, customers are happy. They don't want to pay 10x as much for
> a player programmed in Ada.
This assumes that the player written in Ada would work much better... an
unfouned assumption.
> And on the internet you can quickly roll
> out updates, which also feeds (crappy or streamlined, you pick the term)
> dev and test processes.
Yes.
> For security code one really needs to seek to affirm the absence of
> bugs, rather than checking for their presence and saying "ok" if none
> are noticed. The code should preferably be treated as a mathematical
> object that one can prove theorems about, rather than an engineering
> artifact whose behavior can only be inferred from observing some tiny
> fragment of the state space.
It's not just the code itself.
>> Yes, it [OpenSSL] still is way too big... I hope they don't stop at
>> throwing out half of the code.
>
> One of the guys hacking code out of OpenSSL at a big web site recently
> told me they really do need a lot of the bloaty-looking code in it, that
> deals with buggy browsers, weird certificates, etc.
They are taking the Postel principle way too far here. A widely used
encryption software can be used to sanitize the Internet from these things:
Fail on the weird certificates, let the buggy browers fail, too. This
causes people to notice the bugs, and fix them.
This is like proof-of-the-concept attacks security experts often are
required to write to kick some asses and make sure people start doing
something. People are lazy. If you work around their bugs, they are happy.
Don't. Make them comply.
In security, the Postel principle is simply wrong. You have to aim at zero
bugs, and therefore, you must have a zero tolerance attitude. This is the
exact opposite of the Postel principle.
>>> In the real world you have to interoperate with the stuff that's out
>>> there.
>> No, the stuff out there doesn't work and needs to be replaced, for god's
>> sake! In the real world, you have people and machines who communicate,
>> and apps who had no compatibility whatsoever with existing protocols like
>> WhatsApp did have 100 million customers after a few years.
>
> That works when all endpoints of the application are controlled by a
> single organization. The issues with SSL are more like those of email
> or IPv4, where many independently controlled entities communicate with
> each other. If you want to design science fiction solutions for future
> generations, that's great as long as you recognize what it is. If you
> want to solve today's problems today, that means dealing with the stuff
> that's out there.
The stuff that's out there is the problem.
>> This assumption that you have to stick with the heapload of shit that's
>> out
>> there has been proven wrong quite often. You have situations where you
>> need interoperability, and you have situations where you don't need that.
>
> In an odd (and bad) way, the desktop computer world is actually
> converging towards everything being controlled by one organization
> (i.e. Google). We don't even see word processors, spreadsheets, or
> email clients on desktops any more. It's all Gmail and Google Docs.
> Nobody is willing to install desktop apps these days.
That's not true. A lot of people do install things like Google Drive and
DropBox, where the brower can't do everything. The reason why people use
Google Docs is that the cloud is so much more comfortable. And that's the
reason why they install DropBox: It makes their different devices
interoperate without problems.
The fact that sendind all your data through Google means sending all your
data through the NSA is something people like to ignore.
> It may be a little different in the mobile space, where people will
> install unlimited spyware from "app stores"--that's how Whatsapp got
> around. Getting to that level of popularity isn't easy though, and even
> 100 million is only a few percent of the internet's users. Browsers
> with SSL reach close to 100%.
I was talking about how long it took to get there. Browsers with SSL took
way longer to reach the 100 million users. SSL is about 20 years old, it is
computer stone age.
>> The world outside I need to bother about is that I must pass through the
>> routers that constitute the current Internet. I use UDP for that.
>
> I'm amused by the terrifying vision of enough applications migrating to
> browsers, simultaneously with net2o succeeding, so we end up with
> in-browser net2o stacks written in Javascript.
Haha.
>> [SSL] is broken in so many ways that we have to replace it. It can't
>> be fixed from within, the spec is already broken beyond repair (things
>> like the CA system),
>
> The CA system is still with us because alternatives haven't fared better
> in implementing SSL's goals. It's not especially a technical weakness
> of SSL. I'd like to know how net2o is going to solve this problem.
> Replace SSL CA's by making people go to key signing parties before they
> can buy shoes online?
No. The PGP signing party model is even older and more broken than the PGP
model. We can do a lot better now. The first thing to realize is that the
far easier SSH model ("remember the first contact") is already far better
than the CA system. It is not perfect, but at least an attacker must be
persistent ("captive environment"), and really intercept every connection.
However, we know that SSL's CA system in a captive environment doesn't work,
either: Some CAs have issued wildcard certificates for exactly those boxes
that do DPI and filter the traffic for captive environments (usually inside
a company or a totalitarian country).
The next problem is that the CA system solves a problem that doesn't need
solving: It is caused by the fact that the way to find the shop is not
related to its key. That's not the case in net2o: To find the shop, and
make contact, you already need to know the key. You might have got that
from a QR coded ad (bad idea: pranksters might have replaced that QR code),
or from a shop search engine and price comparison page on the Internet. So
that one would establish a trust chain, and the good thing is: You can use
several trust chains to increase the strenght. If the shop is found in
serveral price search sites, and its key is identical, your trust level can
be much higher.
>> and the glacial speed it has had in the past to improve known spec
>> bugs (like adaption of TLS 1.2 to over TLS 1.0 and SSL3)
>
> I'll be interested to know how quickly net2o protocol changes are
> deployed, once there are hundreds of implementations, and it's running
> in billions of mobile phones (many of them obsolete and no longer
> receiving updates), home routers, industrial machinery, etc.
The net2o I'll implement will include an update path (and I won't certify
anything without such an update path as "net2o compatible and secure").
It's actually pretty trivial, because it's just sharing stuff - this is a
functionality net2o comes with anyways, and the encryption stuff assures you
that you get the updates from the same party you got the original version.
In any case: If the update path feature is missing, the security is already
compromised. Since net2o will contain a distribution tree for things like
Justin Bieber's tweets, the estimation is that a small patch can spread to
every net2o user on the entire planet in less than a second (i.e. to
billions). This stuff happens by combining all those things that are
necessary anyways.
>>> Don't forgot the requirement that it perform comparably to OpenSSL,
>> It performs far better. I know that performance is important,
>
> OK, I see it uses Donna (ECC implementation) rather than a Forth
> implementation, so fine, other stuff can be handled similarly. Note
> there are faster ECC implementations than Donna now.
Which one? I'm deliberately using Dan Bernstein's Ed25519 curve, because
it's signature algorithm doesn't have the random number design problem of
ECDSA, and the implementation is fast. Dan Bernstein's SUPERCOP code is
slightly faster, but non-portable, as it is written in assembler.
>> I wouldn't even considder something with the performance of OpenSSL to
>> be a contender. The competition is unencrypted communication, which
>> is still used by a lot of people.
>
> That's mostly because of deployment and configuration hassles rather
> than performance.
Maybe; however, a lot of web sites used RC4 only because it was fastest.
Performance does matter. Of course, configuraton hassles are to be avoided
at all costs, too. This thing has to work out of the box.
>>>Python, Lisp, or Erlang>
>> Yes, these programming languages are all interactive. If you cherry-pick
>> languages that have similar features as Forth on a particular topic, you
>> will get similar results.
>
> Well yes, you claimed Forth's interactivity was supposed to prevent
> bugs. I listed other interactive languages to indicate it's still quite
> possible to deploy buggy code despite the availability of interaction.
Non-conclusive logic: Interactive languages makes it more fun to squash out
bugs.
>>> The bugs of course usually manifest as non-catastrophic runtime
>>> exceptions,
>>
>> Why do people always think that a runtime exception is non-catastrophic?
>> The famous Ariane 5 debacle was caused by "non-catastrophic runtime
>> exceptions".
>
> What? No, that one was catastrophic and tools like SPARK put a lot of
> emphasis into proving that code is exception-free, for use in critical
> realtime systems. But we're talking about internet protocols, which are
> not realtime in the same way, and where applications must allow that the
> internet itself is inherently unreliable.
Yes.
> If (say) a Java SSL stack
> throws an exception on someone trying a Heartbleed exploit, the result
> is that client experiencing a dropped connection, which is probably what
> you want anyway (plus you get a traceback in the server log and maybe an
> accompanying pager alert, rather than having the bug go unnoticed for
> years).
Maybe you want the client to renegotiate so that you can inject some MITM
attack which is only possible for renegotiation? We had bugs in SSL where
the exploit was exactly this sort of operation.
>> A runtime exception which stops the usual flow, and which isn't
>> properly handled, can be catastrophic for a secure network protocol.
>> An unexpected runtime exception quite likely won't be properly
>> handled.
>
> If the protocol is any good it has to be able to handle someone
> maliciously intercepting the connection and maybe even inserting their
> own data. If you treat exceptions (normally those will come from the
> i/o system) as similar to someone cutting the wire (i.e. report an
> error and give up), you're most of the way towards a sensible solution.
Ok, two things here: If you receive a packet that doesn't decrypt well, you
have to drop that packet and continue as if there wasn't anything.
Otherwise, you make it dead easy for someone to DoS you. If you receive a
packet that does decrypt (and the checksum is ok), you can assume that it
did originate from your communication partner. If there is something inside
that packet that is fishy, and not according to the protocol, you can indeed
just cut the wire and mark that communcation partner as "fishy".
>>> The Haskell QuickCheck tool (basically an automatic fuzz tester)
>> Fuzz testers have their place, but the usually way to go is that you
>> first
>> have to make your program *work* at all. That phase requires injecting
>> known good data, and observing what happens.
>
> Yes, and you have to test at the edge values, which are not always so
> easy to figure out, especially if you're the code author and if you over
> looked something in coding you're likely to also overlook it in testing.
And then you are also likely not to specify the properties to check that
problematic edge of your code...
> The cool thing about QuickCheck is you write the desired properties as
> the test, and QuickCheck itself generates the values, doing a reasonable
> job at guessing the edge cases itself, using Haskell's fine-grained type
> system to determine the possible good values. It frequently hits stuff
> that manual testing misses.
Sounds good. And it follows the idea that you need to know your object
under test to actually produce the tests. A question would be: Could we
adapt that sort of testing to Forth? Maybe together with an analytical
compiler to produce efficient code? That compiler performs enough analysis
of the code to know the stack effect, so it can compare that to the
documentation (which is a specification). It also could extract values that
cause conditions to go either one or the other way.
Usually, the thing with Forth's one-liners however is that you have complete
oversight.
>> Maybe the boilerplate fillers don't like doing this with interactive
>> testing, i.e. a "test first" strategy, where you write a test which
>> you can't run, because the program under test hasn't been written yet.
>
> I'm not sure what you're getting at here. What happens when you
> refactor the program? Do you have to interactively re-test all the
> words?
No, the point here is that you need your object under test to develop the
tests, see your Haskell thing above. The opposite of "write the tests
first" is not "don't write any regression tests". Of course, when I
refactor some parts of my program, I need to test the refactored definitions
and run the integration tests. Serious refactoring often comes with a
changed API, so the old unit tests don't work anymore, either. The
integration tests still should work.
>> No, the thing you really need first is that you don't end up with a
>> big program.
>
> Nice work if you can get it.
It requires an unforgiving attitude at making things simple.
--
Bernd Paysan
"If you want it done right, you have to do it yourself"
http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2014-06-05 15:34 +0000 |
| Subject | Formal specifications etc. (was: MSP430-Stamp) |
| Message-ID | <2014Jun5.173405@mips.complang.tuwien.ac.at> |
| In reply to | #31203 |
Bernd Paysan <bernd.paysan@gmx.de> writes:
>What I think can be done better is the specification stuff.
>Actually the thinking that you should use a formal method to write down your
>spec is *right*. Fundamentally *right*. That's not what I'm going to argue
>about. The wrong here is that you have to write the formal spec, which is
>actually a programming language of sorts (as it is formal and has a well-
>defined semantics), and *then* have to write it again in another programming
>language (the implementation language). Don't. Instead try to compile your
>formal language; this is quite often possible, way more often than you think
>(e.g. Verilog was originally designed as specification language to formally
>verify hand-drawn circuits; but it soon was compiled instead). Or better:
>Make a formal language that allows you to specify your problem easily, i.e.
>a DSL.
>
>The "say things only once" contradicts the formal spec. You should really
>say things only once, and thus you must spend the effort (i.e. writing a
>DSL) to be able to say things only once. The code you use to solve your
>problem must be close to what you expect from a specification language.
I have not read the paper, and I don't believe in the old idea that
formal specifications combined with formal verification produce
correct software (it produced software with requirements bugs and
specification bugs, if it produces any software at all).
But I do think that an additional (redundant) encoding of (some)
requirements (in addition to the executable code or executable
specification) can reduce bugs, especially if the additional encoding
is quite different from the executable code. The idea is that you
will hopefully produce different bugs in the additional encoding, and
you check the additional stuff against the executable code.
I don't think that a formal full specification is cost-effective for
that for most software, but a formal partial specification (i.e.,
specification of some properties and invariants) has been used
successfully (the poster child is Microsoft's use of model checking
for verifying some properties of Windows device drivers), but there
are also other ways, including assertions and test cases (however, in
test-driven development the code is not produced independently of the
test cases, so there bugs in the test cases may become part of the
executable code).
The benefit is that such partial stuff is easier to produce than
formal full specifications, easier to understand, and also easier to
check against the executable code.
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2014: http://www.euroforth.org/ef14/
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2014-06-05 11:48 -0700 |
| Subject | Re: Formal specifications etc. |
| Message-ID | <7xmwdryyy5.fsf@ruckus.brouhaha.com> |
| In reply to | #31207 |
anton@mips.complang.tuwien.ac.at (Anton Ertl) writes: > I have not read the paper, and I don't believe in the old idea that > formal specifications combined with formal verification produce > correct software (it produced software with requirements bugs and > specification bugs, if it produces any software at all). I think we have to admit by now that verification technology has gotten a lot better than it was in the old days. The vision of using it on everything is not currently practical and may never be practical. > But I do think that an additional (redundant) encoding of (some) > requirements (in addition to the executable code or executable > specification) can reduce bugs, especially if the additional encoding > is quite different from the executable code. One of the gains is that you write the specification in one place and then it's enforced on the entire program. The familiar style of static typechecking is an example of this: if the function signature says it takes an integer arg, the compiler verifies that it never receives a string, from any call site. A specification like "N < 100" on an array index is also easy to write, and being able to statically enforce it means you can guarantee that the program won't overflow that array. That is obviously very valuable if you can do it. The difficulty is in the verification (requiring analyzing the whole program to check all the places N might have come from), not in writing the spec. > I don't think that a formal full specification is cost-effective for > that for most software, Sure, certainly true. There is a formally verified TLS, though it doesn't have enough features to be really useful: http://www.mitls.org/wsgi/download
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2014-06-05 19:46 +0000 |
| Subject | Re: Formal specifications etc. |
| Message-ID | <2014Jun5.214601@mips.complang.tuwien.ac.at> |
| In reply to | #31212 |
Paul Rubin <no.email@nospam.invalid> writes:
>anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:
>> I have not read the paper, and I don't believe in the old idea that
>> formal specifications combined with formal verification produce
>> correct software (it produced software with requirements bugs and
>> specification bugs, if it produces any software at all).
>
>I think we have to admit by now that verification technology has gotten
>a lot better than it was in the old days.
Maybe, but that does not solve the fundamental problem: It does not
help against requirement bugs nor against specification bugs.
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2014: http://www.euroforth.org/ef14/
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2014-06-05 23:02 +0200 |
| Subject | Re: Formal specifications etc. (was: MSP430-Stamp) |
| Message-ID | <lmqltb$vt7$1@online.de> |
| In reply to | #31207 |
Anton Ertl wrote: > I have not read the paper, and I don't believe in the old idea that > formal specifications combined with formal verification produce > correct software (it produced software with requirements bugs and > specification bugs, if it produces any software at all). The successful formal verification language I know (especially Verilog) make sense, because you write a lot less than in the actual implementation language (at least that's how it was originally envisioned), and then someone makes a compiler so that you don't have to implement things - the formal verification language itself is enough. There are other approaches at formal verification, through clauses and theoreme prover instead of through identity (Coq vs. Verilog). > But I do think that an additional (redundant) encoding of (some) > requirements (in addition to the executable code or executable > specification) can reduce bugs, especially if the additional encoding > is quite different from the executable code. The idea is that you > will hopefully produce different bugs in the additional encoding, and > you check the additional stuff against the executable code. I've done some formal verification stuff during the "large programming system" lecture on University. That stuff was using the typical formal attributes e.g. Coq now uses (though not as elaborated), comparing against an imperative implementation language. My experience was that you easily forgot clauses that would matter if you implemented it wrong, so this thing was not a "fragile" approach, where mistakes would easily show up, but "robust", i.e. your program might work even though the spec was incomplete, or you wouldn't find the corner-case bugs, because your formal spec wouldn't have the conditions for these corner cases either. Finding a complete set of clauses that really nailed down the formal spec was considerably harder than implementing and testing the code. Omitting a clause would not cause the theoreme prover to fail, because there isn't a 1:1 relation between spec and implementation (unlike Verilog, where you prove identity). > I don't think that a formal full specification is cost-effective for > that for most software, but a formal partial specification (i.e., > specification of some properties and invariants) has been used > successfully (the poster child is Microsoft's use of model checking > for verifying some properties of Windows device drivers), but there > are also other ways, including assertions and test cases (however, in > test-driven development the code is not produced independently of the > test cases, so there bugs in the test cases may become part of the > executable code). The formal spec is usually not written independent, either. Separation of people who write the spec and those who implement it are a big source of friction and errors (especially those who write the spec don't have the feedback from the actual implementation and don't know which tradeoffs to make). > The benefit is that such partial stuff is easier to produce than > formal full specifications, easier to understand, and also easier to > check against the executable code. Let me rephrase: The paper cited has 6 different things in place, and claims to reduce the bug rate by an order of magnitude or even more. Now if you have six things in place, you don't know which of them was how effective, it's like "I cured my cancer by having an operation, chemotherapy, an immune system stimulation through re-implanting gene-modified stem cells, praying to God, drinkig good beer, and fresh flowers on my bed every day." Now find out which one of the 6 things was actually effective, and which one is just a placebo. Paul Rubin quickly jumped on the formal spec (point 1 of 6), because he's believing in that stuff. I'm believing in points 3 to 6 (4 points alltogether), and think the formal spec stuff is mostly a placebo. The paper doesn't mention peer code review, although we know that this quite effective to reduce the number of bugs. To quantize the effect, you have to do all sorts of combinations (maybe some of the bug cures are only effective if applied in combination?), and measure the results. On a number of different projects. -- Bernd Paysan "If you want it done right, you have to do it yourself" http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2014-06-05 14:15 -0700 |
| Subject | Re: Formal specifications etc. |
| Message-ID | <7xppinqcqx.fsf@ruckus.brouhaha.com> |
| In reply to | #31219 |
Bernd Paysan <bernd.paysan@gmx.de> writes: > Paul Rubin quickly jumped on the formal spec (point 1 of 6), because he's > believing in that stuff. I'm believing in points 3 to 6 (4 points > alltogether), and think the formal spec stuff is mostly a placebo. I know that Altran/Praxis puts a lot of emphasis on the spec and verification (they were the original developer and vendor of SPARK, iirc, and they go on about it in other publications). The other stuff in the 6 points certainly matters too. The Tokeneer page[1] has more info and I see now, the 38 loc/day figure really was over the whole length of the project (coding phase was 203 loc/day), so that's impressive. I think I'm reporting what Altron itself believes to be important, whether or not they are right. I haven't used the stuff myself yet, though I've been interested in it. There is some verified crypto stuff here that I've been wanting to look at: http://git.codelabs.ch/?p=spark-crypto.git;a=tree [1] https://www.adacore.com/sparkpro/tokeneer/
[toc] | [prev] | [next] | [standalone]
| From | rickman <gnuarm@gmail.com> |
|---|---|
| Date | 2014-06-05 17:33 -0400 |
| Subject | Re: Formal specifications etc. |
| Message-ID | <lmqno0$v1n$2@dont-email.me> |
| In reply to | #31221 |
On 6/5/2014 5:15 PM, Paul Rubin wrote: > Bernd Paysan <bernd.paysan@gmx.de> writes: >> Paul Rubin quickly jumped on the formal spec (point 1 of 6), because he's >> believing in that stuff. I'm believing in points 3 to 6 (4 points >> alltogether), and think the formal spec stuff is mostly a placebo. > > I know that Altran/Praxis puts a lot of emphasis on the spec and > verification (they were the original developer and vendor of SPARK, > iirc, and they go on about it in other publications). The other stuff > in the 6 points certainly matters too. The Tokeneer page[1] has more > info and I see now, the 38 loc/day figure really was over the whole > length of the project (coding phase was 203 loc/day), so that's > impressive. I think I'm reporting what Altron itself believes to be > important, whether or not they are right. I haven't used the stuff > myself yet, though I've been interested in it. > > There is some verified crypto stuff here that I've been wanting to look at: > > http://git.codelabs.ch/?p=spark-crypto.git;a=tree > > [1] https://www.adacore.com/sparkpro/tokeneer/ Any chance you guys can make a new thread to discuss these things not related to the original subject of MSP430-Stamp? Even though the subject is changed, it is still in the same thread which makes following the original subject hard. -- Rick
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2014-06-05 15:32 -0700 |
| Subject | Re: Formal specifications etc. |
| Message-ID | <7xwqcvhtsj.fsf@ruckus.brouhaha.com> |
| In reply to | #31225 |
rickman <gnuarm@gmail.com> writes: > Any chance you guys can make a new thread to discuss these things not > related to the original subject of MSP430-Stamp? Even though the > subject is changed, it is still in the same thread which makes > following the original subject hard. Hmm, ok. If I post any more about that, I'll start a new thread unless someone else has already started one.
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2014-06-06 04:00 -0500 |
| Subject | Re: Formal specifications etc. |
| Message-ID | <CfOdnb6S6_baHgzOnZ2dnUVZ8n6dnZ2d@supernews.com> |
| In reply to | #31221 |
Paul Rubin <no.email@nospam.invalid> wrote: > > I know that Altran/Praxis puts a lot of emphasis on the spec and > verification (they were the original developer and vendor of SPARK, > iirc, and they go on about it in other publications). No. SPARK was developed by Southampton University and Program Validation Limited, also of Southampton. Andrew.
[toc] | [prev] | [next] | [standalone]
| From | albert@spenarnc.xs4all.nl (Albert van der Horst) |
|---|---|
| Date | 2014-06-06 11:05 +0000 |
| Subject | Re: Formal specifications etc. (was: MSP430-Stamp) |
| Message-ID | <5391a079$0$4852$e4fe514c@dreader35.news.xs4all.nl> |
| In reply to | #31219 |
In article <lmqltb$vt7$1@online.de>, Bernd Paysan <bernd.paysan@gmx.de> wrote: <SNIP> >it's like "I cured my cancer by having an operation, chemotherapy, an immune >system stimulation through re-implanting gene-modified stem cells, praying >to God, drinkig good beer, and fresh flowers on my bed every day." Now find >out which one of the 6 things was actually effective, and which one is just >a placebo. Big mistake here. Placebo's *are* effective and actually cure people. That is why they annoy the behezus out of the traditional medicine people. <SNIP> >-- >Bernd Paysan -- Albert van der Horst, UTRECHT,THE NETHERLANDS Economic growth -- being exponential -- ultimately falters. albert@spe&ar&c.xs4all.nl &=n http://home.hccnet.nl/a.w.m.van.der.horst
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2014-06-05 11:01 -0700 |
| Message-ID | <7xzjhrz15q.fsf@ruckus.brouhaha.com> |
| In reply to | #31203 |
Bernd Paysan <bernd.paysan@gmx.de> writes:
> The wrong here is that you have to write the formal spec, which is
> actually a programming language of sorts (as it is formal and has a
> well- defined semantics), and *then* have to write it again in another
> programming language (the implementation language). Don't. Instead
> try to compile your formal language; this is quite often possible, way
> more often than you think
Sure. In the limit though, this is called automatic theorem proving and
it's "AI-complete".
> (e.g. Verilog was originally designed as specification language to
> formally verify hand-drawn circuits; but it soon was compiled
> instead).
That's not easy though: Verilog compilers do a heck of a lot of work,
especially if you consider the "output" to be rectangles, so compilation
includes place-and-route. Yes it's awesome how well that problem has
been solved but it's much easier to specify a chip's function (in
Verilog) than to actually render it.
> Or better: Make a formal language that allows you to specify your
> problem easily, i.e. a DSL.
Specifying the problem is of course not the same as solving it. Think
of two Forth words (predicates on integers):
: w1 ( n -- flag ) .... ;
: w2 ( n -- flag ) .... ;
You can specify a property called "equivalence" on two words with this
signature: they are equivalent iff for all inputs they produce the same
output. For example, w1 and w2 might both test whether n is a prime
number using completely different algorithms. The equivalence spec
captures that they both compute the same thing. Now imagine you've
got a function that operates on fragments of machine code:
: optimize ( xt1 -- xt2 )
\ SPECIFICATION: xt1 and xt2 are equivalent ... ;
This is a compiler optimization pass that takes a chunk of code and
returns an "improved" chunk that does the same thing. Maybe it's
"buggy" in the sense that the new code is slower than the old code
rather than faster, but if the equivalence spec is verified, the
optimization can't introduce an actual wrong-code bug. This is
basically how CompCert works: it has a series of code transformations
that are all verified to satisfy input-output equivalence in the above
sense. So we get papers like http://mehrdadafshari.com/emi/paper.pdf
which introduce methodology that finds hundreds of codegen bugs in GCC
and LLVM, but not a single one in CompCert.
What's not so easy, of course, is generating those transformations and
equivalence proofs automatically, given just the spec. Humans are still
in the loop.
> The "say things only once" contradicts the formal spec. You should really
> say things only once, and thus you must spend the effort (i.e. writing a
> DSL) to be able to say things only once. The code you use to solve your
> problem must be close to what you expect from a specification language.
SQL is a successful near-example of this, but the approach runs out of
gas after a while. The Altran guys use Z notation for specifications,
which is based on set theory, then they code in SPARK/Ada. In Haskell
or Coq, the "specifications" are type signatures, so they're part of the
language, but the types don't really look that much like the "term"
language (that gets compiled to executable code).
> The zero-defect example that they list in the end of the article is just
> 10kLoCs, and it was written quite fast (38LoCs/day is really fast).
The second article discusses the Mondex wallet which is around 100 KLOC.
The Tokeneer code is here, btw: https://www.adacore.com/sparkpro/tokeneer/
I think the 38 LOC/day might just be the coding phase of the project,
which is a somewhat bogus because of the longer-than-usual design and
prototype phase. To compare process productivity you really have to
compare start-to-finish times of entire projects. But, I don't mind the
idea that a high-assurance process takes longer than a lolcat process
(where it's reasonable to expect 100+ loc/day with good coders). The
interesting thing is that these verification methods were known in the
1970's or 80's and were considered impractical then, but they're
relatively accessible now, and yet most programmers still think they're
impractical (rather than just somewhat specialized).
> Nope. Spilling keys is just as bad as e.g. not detecting a MITM attack.
Of course spilled keys are worse: they enable the MITM attack whether or
not the attack is present in the protocol implementation, and they
enable it for all future sessions that use the same authentication key,
even if the implementation is patched. And if the protocol lacks
forward secrecy or accidentally persists keys (think of session caches),
the spilled key can even reveal past traffic from before the MITM got
in.
> The assumption that Java helps you to avoid crazy stuff IMHO is completely
> unfounded.
It avoids so-called "nasal demons" of which spilling keys in Heartbleed
was an example.
>> told me they really do need a lot of the bloaty-looking code in it, that
>> deals with buggy browsers, weird certificates, etc.
>
> They are taking the Postel principle way too far here. A widely used
> encryption software can be used to sanitize the Internet from these things:
> Fail on the weird certificates, let the buggy browers fail
Like most businesses they are more interested in satisfying their
customers than "sanitizing the internet". If each rejected browser or
certificate results in angry customers and piles of support tickets, and
those browsers and certs work perfectly well with other servers, then
they have strong motivation to also handle those browsers and certs.
>> Nobody is willing to install desktop apps these days.
> That's not true. A lot of people do install things like Google Drive
> and DropBox, where the brower can't do everything....: It makes their
> different devices interoperate without problems.
Hmm, yeah, I forgot about that due to being suspicious of the downloads
and not using a lot of devices, plus having relatively slow internet and
knowing how to use upload programs. I just use git or rsync for
synchronization.
> The fact that sendind all your data through Google means sending all
> your data through the NSA is something people like to ignore.
Even if it's not going to the NSA, it's still going to Google.
> the far easier SSH model ("remember the first contact") is already far
> better than the CA system. It is not perfect, but at least an
> attacker must be persistent ("captive environment"), and really
> intercept every connection.
I don't think so, it's bad enough if they intercept just the first
connection, if that's the only connection. E.g. you're in a wifi cafe
with MITM and you connect to a new site for the first and only time.
Even if you connect again later and discover the changed key, what are
you going to do about it? What happens if you connect to an sshd that
you use regularly, except this time the key has changed? Most of us
just figure the sysadmin has changed the key for some reason, and say
"yes" to accept it. Not good.
> Some CAs have issued wildcard certificates for exactly those boxes
> that do DPI and filter the traffic for captive environments (usually
> inside a company or a totalitarian country).
I don't think any preinstalled CA's can admit to that and survive. The
ones inside companies involve browsers on company computers, configured
by the company to accept the MITM certificate. Since the company also
controls all the software on the computer, SSL MITM isn't particularly a
point of vulnerability.
The CA system works reasonably well for its intended purpose, the online
shoe store model where compromising millions of sessions (by
intercepting traffic at the server) is disastrous but compromising a few
individual sessions is only annoying (person has to get a new credit
card, bank has to pay for any monetary losses and they build occasional
such losses into their existing cost structure). It's more problematic
in the gmail model where each session is its own potential spy story
that could start a war or whatever. Extensions like TACK can indeed
help with this.
>> there are faster ECC implementations than Donna now.
> Which one? I'm deliberately using Dan Bernstein's Ed25519 curve,
There are several people who claim to have them, I haven't tracked
specific implementations but there might be some info in the curves
mailing list archive at moderncrypto.org. The messaging list on the
same site would be a cool place for you to send something about net2o,
by the way.
> Non-conclusive logic: Interactive languages makes it more fun to
> squash out bugs.
You know, I don't really find this. I find interactive debuggers
helpful (I know that you don't). Interactive languages are nice when I
don't understand the API of some library I want to use, so I want to try
stuff and poke at it. For code where I understand what's already there,
careful coding and/or TDD seems to help more than interactivity.
> Maybe you want the client to renegotiate so that you can inject some MITM
You're in trouble if any version of the protocol allows MITM.
> Ok, two things here: If you receive a packet that doesn't decrypt
> well, you have to drop that packet and continue as if there wasn't
> anything. Otherwise, you make it dead easy for someone to DoS you.
Ehh, if they can mess with packets they can already DOS you.
>> QuickCheck itself generates the values... using Haskell's
>> fine-grained type system to determine the possible good values.
>
> Sounds good. ... A question would be: Could we adapt that sort of
> testing to Forth? Maybe together with an analytical compiler to
> produce efficient code? That compiler performs enough analysis of the
> code to know the stack effect, so it can compare that to the
> documentation (which is a specification).
Typical Forth stack comments probably don't have enough info to be much
help: for example, the test generator might not figure out that "addr u"
is supposed to be a character string. And I get the impression that
wrong stack effects already aren't a frequent source of bugs in Forth
code (are they?) and they can usually be checked statically without any
tests. Peter Knaggs' PhD thesis (it's online someplace) discusses how
to write more specific Forth signatures that sort of resemble Haskell
types. Maybe that's worth looking into for test generation.
> Usually, the thing with Forth's one-liners however is that you have
> complete oversight.
Well with QuickCheck (or other testing) you exercise the entire call
tree under the one-liner.
> No, the point here is that you need your object under test to develop
> the tests, see your Haskell thing above. The opposite of "write the
> tests first" is not "don't write any regression tests".
You can still write the tests first, and doing that helps make the
design testable, it's not boilerplate filling. I find it useful for
some types of code (mostly in Python).
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2014-06-06 01:09 +0200 |
| Message-ID | <lmqtan$l3o$1@online.de> |
| In reply to | #31209 |
Paul Rubin wrote:
>> (e.g. Verilog was originally designed as specification language to
>> formally verify hand-drawn circuits; but it soon was compiled
>> instead).
>
> That's not easy though: Verilog compilers do a heck of a lot of work,
> especially if you consider the "output" to be rectangles, so compilation
> includes place-and-route. Yes it's awesome how well that problem has
> been solved but it's much easier to specify a chip's function (in
> Verilog) than to actually render it.
No, been there, done that. A lot of electric engineers think that the
Verilog compiler can't produce something good and meaningful out of my
mostly straight-forward pretty high-level description (e.g. the b16
processor). I've been told that the synthesis tool won't produce what I'm
intending. I've looked, it did. The compilation is broken into steps, so
that place-and-route is actually a different operation, and BTW all those
steps have equivalence provers to check that they are done correct (formal
verification to compare RTL to netlist, and Layout vs. Schematic (LVS) to
compare the place&route result to the netlist.
>> Or better: Make a formal language that allows you to specify your
>> problem easily, i.e. a DSL.
>
> Specifying the problem is of course not the same as solving it. Think
> of two Forth words (predicates on integers):
> : w1 ( n -- flag ) .... ;
> : w2 ( n -- flag ) .... ;
> You can specify a property called "equivalence" on two words with this
> signature: they are equivalent iff for all inputs they produce the same
> output. For example, w1 and w2 might both test whether n is a prime
> number using completely different algorithms. The equivalence spec
> captures that they both compute the same thing. Now imagine you've
> got a function that operates on fragments of machine code:
>
> : optimize ( xt1 -- xt2 )
> \ SPECIFICATION: xt1 and xt2 are equivalent ... ;
Ouch. If you had followed our discussion with Andrew (representing the GCC
team, a bad job he has here ;-), you'll immediately see that "equivalent" is
something that is pretty hard to define. Because there are these
"undefined" results...
Take your prime number example above: For calculating RSA key primes, you
use a probabilistic test for prime. This probabilistic test will never
report a prime as non-prime, but will give false positives. So all you do
is to repeat the test until you are sufficiently sure that it is a prime.
There is still a (small) likelyhood that you are wrong.
This stuff is used in crypto software. The specification for RSA of course
is "For an n bit key choose two different randomly chosen prime numbers p
and q with n/2 bits each". Of course the programs formally never will meet
that spec, because a probabilistic prime number test has a likelyhood of
failure.
> This is a compiler optimization pass that takes a chunk of code and
> returns an "improved" chunk that does the same thing. Maybe it's
> "buggy" in the sense that the new code is slower than the old code
> rather than faster,
That wouldn't be hard, just specify that there is a total order, and the new
code has to be at least as fast as the old code.
> but if the equivalence spec is verified, the
> optimization can't introduce an actual wrong-code bug. This is
> basically how CompCert works: it has a series of code transformations
> that are all verified to satisfy input-output equivalence in the above
> sense. So we get papers like http://mehrdadafshari.com/emi/paper.pdf
> which introduce methodology that finds hundreds of codegen bugs in GCC
> and LLVM, but not a single one in CompCert.
I'm surprised that the Clang and GCC team actually confirmed and fixed 2/3
of these bugs. The remaining are probably all "invalid" ;-).
> What's not so easy, of course, is generating those transformations and
> equivalence proofs automatically, given just the spec. Humans are still
> in the loop.
IMHO, you are picking something that is a very good target for formal
methods, because it actually does an equivalence transformation: The
optimizing backend of a compiler. I've argued about not using Formality (a
RTL vs. netlist comparison tool) on a project that had a very tight
deadline, because it actually verifies that the Verilog compiler isn't
producing bullshit, and we were confident that the Verilog compiler was good
enough - never found a miscompilation in years.
And I'm really scared that this sort of tool is not available for verifying
software compilers. There are two reasons for having such a tool:
1. Debugging the compiler (and they need a lot of debugging), and
2. checking binaries for hidden backdoors (see Ken Tompson's stone-age paper
about compiler security...)
>> The zero-defect example that they list in the end of the article is just
>> 10kLoCs, and it was written quite fast (38LoCs/day is really fast).
>
> The second article discusses the Mondex wallet which is around 100 KLOC.
> The Tokeneer code is here, btw: https://www.adacore.com/sparkpro/tokeneer/
>
> I think the 38 LOC/day might just be the coding phase of the project,
> which is a somewhat bogus because of the longer-than-usual design and
> prototype phase. To compare process productivity you really have to
> compare start-to-finish times of entire projects. But, I don't mind the
> idea that a high-assurance process takes longer than a lolcat process
> (where it's reasonable to expect 100+ loc/day with good coders). The
> interesting thing is that these verification methods were known in the
> 1970's or 80's and were considered impractical then, but they're
> relatively accessible now, and yet most programmers still think they're
> impractical (rather than just somewhat specialized).
>
>> Nope. Spilling keys is just as bad as e.g. not detecting a MITM attack.
>
> Of course spilled keys are worse: they enable the MITM attack whether or
> not the attack is present in the protocol implementation, and they
> enable it for all future sessions that use the same authentication key,
> even if the implementation is patched. And if the protocol lacks
> forward secrecy or accidentally persists keys (think of session caches),
> the spilled key can even reveal past traffic from before the MITM got
> in.
Ok, I think of non-forward secrecy protocols as broken anyways ;-). That is
because there are other ways to get a constant key than just a bug in the
implementation...
>> The assumption that Java helps you to avoid crazy stuff IMHO is
>> completely unfounded.
>
> It avoids so-called "nasal demons" of which spilling keys in Heartbleed
> was an example.
Are you sure of that? The problem with Heartbleed and OpenSSL is that it
had its own malloc, because someone found a reason to avoid using the
system's malloc - that's why tools like Valgrind didn't find a problem. Now
guess if this sort of stupid design decision would have been made in Java:
Instead of using Java's native objects to store data, the hypothetical
jOpenSSL developers would have allocated 64k ByteArrays and implement their
own storage management on top of those...
Yes, really, that's the sort of code quality we are discussing here. It's
like you use Forth, and stop passing addr u as buffers because you think
this takes too much stack space. And then you end up with a buffer
overflow... People who try that sort of stuff will manage to expose their
keys in Coq. Provable (if you add the rule to show the proof ;-).
>>> told me they really do need a lot of the bloaty-looking code in it, that
>>> deals with buggy browsers, weird certificates, etc.
>>
>> They are taking the Postel principle way too far here. A widely used
>> encryption software can be used to sanitize the Internet from these
>> things: Fail on the weird certificates, let the buggy browers fail
>
> Like most businesses they are more interested in satisfying their
> customers than "sanitizing the internet". If each rejected browser or
> certificate results in angry customers and piles of support tickets, and
> those browsers and certs work perfectly well with other servers, then
> they have strong motivation to also handle those browsers and certs.
This is a hypothetical situation, the real situation is that the other SSL
implementations usually choke on a lot more certs than OpenSSL... the
Frankencert study unfortunately shows that the other SSL implementations
choke by *accepting* those broken certificates:
https://www.cs.utexas.edu/~shmat/shmat_oak14.pdf
That is of course worse than accepting a just weird certificate...
The reason here is probably that these other SSL libraries are used in web
servers, and those rarely have to check certificates, so the bugs slip
through.
>>> Nobody is willing to install desktop apps these days.
>> That's not true. A lot of people do install things like Google Drive
>> and DropBox, where the brower can't do everything....: It makes their
>> different devices interoperate without problems.
>
> Hmm, yeah, I forgot about that due to being suspicious of the downloads
> and not using a lot of devices, plus having relatively slow internet and
> knowing how to use upload programs. I just use git or rsync for
> synchronization.
Yes, my reaction to the first person mentioning Dropbox (for exchanging
stuff submitted to our Forth Gesellschaft journal) was "use a DVCS, please!"
But the Dropbox model of watched folders and automatic sync is really a lot
easier for mere users.
>> The fact that sendind all your data through Google means sending all
>> your data through the NSA is something people like to ignore.
>
> Even if it's not going to the NSA, it's still going to Google.
Yes, but at least Google has no prisons and no killer drones (they have
bought a maker of the latter recently, though).
>> the far easier SSH model ("remember the first contact") is already far
>> better than the CA system. It is not perfect, but at least an
>> attacker must be persistent ("captive environment"), and really
>> intercept every connection.
>
> I don't think so, it's bad enough if they intercept just the first
> connection, if that's the only connection. E.g. you're in a wifi cafe
> with MITM and you connect to a new site for the first and only time.
> Even if you connect again later and discover the changed key, what are
> you going to do about it? What happens if you connect to an sshd that
> you use regularly, except this time the key has changed? Most of us
> just figure the sysadmin has changed the key for some reason, and say
> "yes" to accept it. Not good.
Ok, the latter is the key migration problem: I've solved that; it doesn't
require a certificate authority, but can be made 100% secure. The wifi cafe
problem isn't solved in SSL, either (or, let's say: It is broken. What do
you expect the MITM wifi box from the Chinese government will do when you
use SSL? It will present you a certificate signed by the Chinese
authorities, which is part of the root certs in your browser... The
Iranians needed to hack Diginotar to get such a wildcard cert - but they got
it ;-).
>> Some CAs have issued wildcard certificates for exactly those boxes
>> that do DPI and filter the traffic for captive environments (usually
>> inside a company or a totalitarian country).
>
> I don't think any preinstalled CA's can admit to that and survive.
They did. They simply were too big to fail, or for other reasons couldn't
be revoked (like Verisign and GoDaddy who provides wildcard certs for
coroporate MITM firewall suppliances). If you throw out Verisign and
Godaddy, the Internet goes dark. If you take the Chinese authority cert out
of the root cert list in the browser, you can say goodbye to the Chinese
market.
> The
> ones inside companies involve browsers on company computers, configured
> by the company to accept the MITM certificate. Since the company also
> controls all the software on the computer, SSL MITM isn't particularly a
> point of vulnerability.
Yes, that's the idea, and that's how it should work. But BYOD is a trendy
thing, and the makers of those boxes have found ways to deal with it. Scary
ways.
> The CA system works reasonably well for its intended purpose, the online
> shoe store model where compromising millions of sessions (by
> intercepting traffic at the server) is disastrous but compromising a few
> individual sessions is only annoying (person has to get a new credit
> card, bank has to pay for any monetary losses and they build occasional
> such losses into their existing cost structure). It's more problematic
> in the gmail model where each session is its own potential spy story
> that could start a war or whatever. Extensions like TACK can indeed
> help with this.
The Gmail thing fortunately is the one which is easier to solve: The people
you are communicating with are social contacts. People where you can
actually verify their IDs or establish a trust path through other social
contacts. The shoe shop model actually also gives you a way to deal with
the cafe wifi single connection situation: You have to use a communication
with a known and trusted third party, your bank, to complete that
transaction.
The thing that is broken with the CA system is that one single signature
from one of the 600 CAs (including "Turktrust" and the Chinese government,
and the biggest CAs are all subject to NSLs) gives you "trust".
The model I have in mind is that you get trust by asking others, not by
asking the probably MITM-attacked communication partner. The way net2o
addressing works means that when you tell me "go to this site" or "talk to
this guy", you are already giving me the pubkey of the site or the guy,
because you have used it, and stored it in your bookmarks or address book.
>>> there are faster ECC implementations than Donna now.
>> Which one? I'm deliberately using Dan Bernstein's Ed25519 curve,
>
> There are several people who claim to have them, I haven't tracked
> specific implementations but there might be some info in the curves
> mailing list archive at moderncrypto.org. The messaging list on the
> same site would be a cool place for you to send something about net2o,
> by the way.
Yes, thanks. Seems to be rather new.
>> Non-conclusive logic: Interactive languages makes it more fun to
>> squash out bugs.
>
> You know, I don't really find this. I find interactive debuggers
> helpful (I know that you don't). Interactive languages are nice when I
> don't understand the API of some library I want to use, so I want to try
> stuff and poke at it. For code where I understand what's already there,
> careful coding and/or TDD seems to help more than interactivity.
Ok, then make that an issue of taste. I find "careful coding" conter-
productive and not fun. Usually, I write way too much stuff when "carefully
coding". I'm very nervous when making big changes, I prefer to make small
changes and then check. Check can mean run a prepared test (that's usually
when refactoring), or test interactively (that's when I test newly written
stuff). Once it's solid enough and I understand what I'm doing, I can start
putting regression tests into a file.
Trying stuff and poking at things happens IMHO quite often.
>> Maybe you want the client to renegotiate so that you can inject some MITM
>
> You're in trouble if any version of the protocol allows MITM.
Sure. The thing is that this sort of bug is not caught by some typechecking
or such. Just today, we had another OpenSSL bug in this class - mess with a
connection during setup so that both sides will switch to a very week
encryption.
>> Ok, two things here: If you receive a packet that doesn't decrypt
>> well, you have to drop that packet and continue as if there wasn't
>> anything. Otherwise, you make it dead easy for someone to DoS you.
>
> Ehh, if they can mess with packets they can already DOS you.
You know, you can fake the sender on the current Internet...
>>> QuickCheck itself generates the values... using Haskell's
>>> fine-grained type system to determine the possible good values.
>>
>> Sounds good. ... A question would be: Could we adapt that sort of
>> testing to Forth? Maybe together with an analytical compiler to
>> produce efficient code? That compiler performs enough analysis of the
>> code to know the stack effect, so it can compare that to the
>> documentation (which is a specification).
>
> Typical Forth stack comments probably don't have enough info to be much
> help: for example, the test generator might not figure out that "addr u"
> is supposed to be a character string. And I get the impression that
> wrong stack effects already aren't a frequent source of bugs in Forth
> code (are they?)
No, not really. But if you want to go down from 1 bug per kLoC to 0.01 bug
per kLoC, you may include those bugs as something you might want to check,
too.
> and they can usually be checked statically without any
> tests. Peter Knaggs' PhD thesis (it's online someplace) discusses how
> to write more specific Forth signatures that sort of resemble Haskell
> types. Maybe that's worth looking into for test generation.
Yes, that sort of thing would be necessary. Some people use "addr len"
instead of "addr u" to specify strings, just to make clear that u is not
just an unrelated integer. There were some discussions to use "addr len" in
Forth200x, but we dropped that.
>> Usually, the thing with Forth's one-liners however is that you have
>> complete oversight.
>
> Well with QuickCheck (or other testing) you exercise the entire call
> tree under the one-liner.
This "complete oversight" stuff is more about that you are putting things
together which are all trustworthy.
>> No, the point here is that you need your object under test to develop
>> the tests, see your Haskell thing above. The opposite of "write the
>> tests first" is not "don't write any regression tests".
>
> You can still write the tests first, and doing that helps make the
> design testable, it's not boilerplate filling. I find it useful for
> some types of code (mostly in Python).
Maybe. The network and encryption stuff I'm doing makes writing test first
pretty hard, because the expected output of some cryptographic function is
not something you can easily calculate. E.g. take the key renewal: You
need to revoke the old key using some signatures and a diffie hellman
exchange for the magic that proves that you made that key; and provide the
new key, which also needs a signature to prove you own it.
The way to deal with that is that I write the code to generate and to check
the revocation together, and then generate revocations, fuzz them, and check
them. The unmodified must pass, any change must cause a failure.
This is incremental: Of course I start with an incomplete renewal, and then
add signatures and checks until it is complete.
--
Bernd Paysan
"If you want it done right, you have to do it yourself"
http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | rickman <gnuarm@gmail.com> |
|---|---|
| Date | 2014-06-05 22:01 -0400 |
| Message-ID | <lmr7eb$vs9$1@dont-email.me> |
| In reply to | #31231 |
On 6/5/2014 7:09 PM, Bernd Paysan wrote: > > This is incremental: Of course I start with an incomplete renewal, and then > add signatures and checks until it is complete. This has drifted pretty far afield from the original topic. Can I ask you guys to start a new thread so we can more easily see more relevant traffic in this thread when it happens? Thanks. -- Rick
[toc] | [prev] | [next] | [standalone]
| From | stephenXXX@mpeforth.com (Stephen Pelc) |
|---|---|
| Date | 2014-05-31 16:47 +0000 |
| Message-ID | <538a0753.278750386@news.demon.co.uk> |
| In reply to | #31070 |
On Sat, 31 May 2014 03:33:46 -0700 (PDT), Mark Wills <markwills1970@gmail.com> wrote: >Correct on all fronts. The VM2 hardware and software is really good. The is= >sue for me is that the software has reached a level of complexity that I am= > uncomfortable with. The type of applications I want a board for are missio= >n critical (SIL-1 or SIL-2). It comes down to being able prove to an extern= >al auditor that your code, or the OS underneath it isn't going to go off in= >to the weeds. That's difficult to do with a closed OS. It's quite easy to d= >o with an OS-less Forth system. Well, you know where we live, and we have a colleague who does safety critical stuff for a living and the the Venom uses a CPU we know about. Regards, Stephen -- Stephen Pelc, stephenXXX@mpeforth.com MicroProcessor Engineering Ltd - More Real, Less Time 133 Hill Lane, Southampton SO15 5AF, England tel: +44 (0)23 8063 1441, fax: +44 (0)23 8033 9691 web: http://www.mpeforth.com - free VFX Forth downloads
[toc] | [prev] | [next] | [standalone]
| From | visualforth@rocketmail.com |
|---|---|
| Date | 2014-05-30 12:11 -0700 |
| Message-ID | <57b3a694-6cf2-4158-a945-4536b9fee448@googlegroups.com> |
| In reply to | #31019 |
On Friday, May 30, 2014 6:12:15 AM UTC-4, Mark Wills wrote: > What I want to see is a small Forth board (MSP430 is > > fine) with a range of add-on boards that can be > > used for real world stuff. > > > > I want relay boards (one board, to drive 8 relays) > > I want analogue boards: 4-20mA current loop type > > (source or sink selectable) > > I want PWM boards > > I want I2C boards > > I want a LCD display add-on > > I want a 16-key keypad add-on > > I want a SD card reader add-on > > > > You know, like Microrobotics, from Cambridge do for > > their Venom boards: > > > > http://microrobotics.co.uk/vm2/interface.html > > http://microrobotics.co.uk/vm2/display.html > > http://microrobotics.co.uk/vm2/starterkit.html > > > > They make an awesome product. If something like that could be done, but with a Forth environment on it, I'm in. Simon could use these boards for his project: "The Industrial I/O cards provide an interface between the controller and industrial signal levels. Up to 16 cards may be daisy-chained on to each I2C bus to form a complete system. The cards plug directly into the I2C connector on any standard Application Board. I2C cable supplied" Source: http://microrobotics.co.uk/vm2/interface.html
[toc] | [prev] | [next] | [standalone]
| From | Matthias Koch <matthias.koch@hot.uni-hannover.de> |
|---|---|
| Date | 2014-06-06 12:54 +0200 |
| Message-ID | <lms6nr$t24$1@newsserver.rrzn.uni-hannover.de> |
| In reply to | #31019 |
Mark Wills schrieb: > You know, like Microrobotics, from Cambridge do for > their Venom boards: > They make an awesome product. If something like that could be done, but with a Forth environment on it, I'm in. This board is based on STM32F103, a chip which is already supported by Mecrisp-Stellaris. Change memory map and maybe choose another UART and you are ready to fly.
[toc] | [prev] | [next] | [standalone]
| From | Matthias Koch <matthias.koch@hot.uni-hannover.de> |
|---|---|
| Date | 2014-06-02 11:39 +0200 |
| Message-ID | <lmhgqn$jk6$1@newsserver.rrzn.uni-hannover.de> |
| In reply to | #30977 |
The discussion here is a lot on "why another board" if you have the Launchpad which is hard to beat in its original price... That is a strong point, but we have something to improve on: * Launchpad terminal is quite an issue. Reflashing the MSP430F1612 with a better firmware and cutting two traces can solve this mostly and gives 115200 target terminal. Mecrisp runs on this chip, and I have done - still unreleased - SBW JTAG bit bang code in Forth. Basically is functional, but sometimes (3-4 times in 10 kb target code written) the Flash write fails, Someone needs to look on this (Flash timing spec violation ?) to make target Flash write more reliable, then it is ready to fly. * Launchpads are brickable if you have no 4 wire JTAG available. * Launchpads are rather big. * Launchpads have no optical link on board. My favourite for a MSP430-Stamp would be a mix of Goodfet ideas (FTDI, unbrickable, flawless fast terminal, usable as JTAG tool) http://goodfet.sourceforge.net/hardware/goodfet42/ and those shiny ATtiny breadboard headers http://tinkerlog.com/2009/01/18/attiny-breadboard-headers/ with an additional optical link onboard. To be included: MSP430G... - either socketed DIP MSP430G2553 or stronger SMD MSP430G2955. Reset button LED FT232RL Diode for power decoupling of FTDI ->|- MSP430 if USB is not connected. Breadboard compatible pin row, but not populated for default And target a more realistic price of around $8-$10. Matthias
[toc] | [prev] | [next] | [standalone]
| From | rickman <gnuarm@gmail.com> |
|---|---|
| Date | 2014-06-02 12:15 -0400 |
| Message-ID | <lmi7ud$mvo$1@dont-email.me> |
| In reply to | #31147 |
On 6/2/2014 5:39 AM, Matthias Koch wrote: > The discussion here is a lot on "why another board" if you have the > Launchpad which is hard to beat in its original price... That is a > strong point, but we have something to improve on: > > * Launchpad terminal is quite an issue. Reflashing the MSP430F1612 with > a better firmware and cutting two traces can solve this mostly and gives > 115200 target terminal. Mecrisp runs on this chip, and I have done - > still unreleased - SBW JTAG bit bang code in Forth. Basically is > functional, but sometimes (3-4 times in 10 kb target code written) the > Flash write fails, Someone needs to look on this (Flash timing spec > violation ?) to make target Flash write more reliable, then it is ready > to fly. > > * Launchpads are brickable if you have no 4 wire JTAG available. I'm unclear on this. How is the LaunchPad brickable when there are dedicated serial port and JTAG controller chips? Are you saying you can brick the JTAG controller MSP430? > * Launchpads are rather big. > > * Launchpads have no optical link on board. > > My favourite for a MSP430-Stamp would be a mix of Goodfet ideas (FTDI, > unbrickable, flawless fast terminal, usable as JTAG tool) > > http://goodfet.sourceforge.net/hardware/goodfet42/ > > and those shiny ATtiny breadboard headers > > http://tinkerlog.com/2009/01/18/attiny-breadboard-headers/ > > with an additional optical link onboard. > > To be included: > > MSP430G... - either socketed DIP MSP430G2553 or stronger SMD MSP430G2955. > Reset button > LED > FT232RL > Diode for power decoupling of FTDI ->|- MSP430 if USB is not connected. > Breadboard compatible pin row, but not populated for default > > And target a more realistic price of around $8-$10. > > Matthias -- Rick
[toc] | [prev] | [next] | [standalone]
| From | Matthias Koch <matthias.koch@hot.uni-hannover.de> |
|---|---|
| Date | 2014-06-03 10:26 +0200 |
| Message-ID | <lmk0tq$c9p$1@newsserver.rrzn.uni-hannover.de> |
| In reply to | #31151 |
>> * Launchpads are brickable if you have no 4 wire JTAG available. > > I'm unclear on this. How is the LaunchPad brickable when there are > dedicated serial port and JTAG controller chips? Are you saying you can > brick the JTAG controller MSP430? > Exactly this. You can abuse the firmware upload mechanism... By the way, there are 5 test points next to the MSP430F1612 on the Launchpad. TP2: Reset TP4: TCK TP5: TMS TP6: TDI TP7: TDO Matthias
[toc] | [prev] | [next] | [standalone]
Page 6 of 10 — ← Prev page 1 … 4 5 [6] 7 8 … 10 Next page →
Back to top | Article view | comp.lang.forth
csiph-web