Search Results: "xam"

7 November 2017

Reproducible builds folks: Reproducible Builds: Weekly report #132

Here's what happened in the Reproducible Builds effort between Sunday October 29 and Saturday November 4 2017: Past events Upcoming events Reproducible work in other projects Packages reviewed and fixed, and bugs filed Reviews of unreproducible packages 7 package reviews have been added, 43 have been updated and 47 have been removed in this week, adding to our knowledge about identified issues. Weekly QA work During our reproducibility testing, FTBFS bugs have been detected and reported by: Documentation updates diffoscope development Version 88 was uploaded to unstable by Mattia Rizzolo. It included contributions (already covered by posts of the previous weeks) from: strip-nondeterminism development Version 0.040-1 was uploaded to unstable by Mattia Rizzolo. It included contributions already covered by posts of the previous weeks, as well as new ones from:
Version 0.5.2-2 was uploaded to unstable by Holger Levsen. It included contributions already covered by posts of the previous weeks, as well as new ones from: reprotest development buildinfo.debian.net development tests.reproducible-builds.org Misc. This week's edition was written by Bernhard M. Wiedemann, Chris Lamb, Mattia Rizzolo & reviewed by a bunch of Reproducible Builds folks on IRC & the mailing lists.

5 November 2017

Thorsten Alteholz: My Debian Activities in October 2017

FTP assistant Again, this month almost the same numbers as last month appeared in the statistics. I accepted 214 packages and rejected 22 uploads. The overall number of packages that got accepted this month was only 339. Debian LTS This was my fortieth month that I did some work for the Debian LTS initiative, started by Raphael Hertzog at Freexian. This month my all in all workload has been 20.75h. During that time I did LTS uploads of: I also took care of radare2 twice and marked all four CVEs as not-affected for Wheezy and Jessie. As nobody else wanted to address the issues in wireshark yet, I now started to work on this package. Last but not least I did one week of frontdesk duties. Other stuff During October I took care of some bugs and at one go uploaded new upstream versions of hoel and duktape (this had to be done twice as I introduced an new bug with the first upload :-(). I only fixed bugs in glewlwyd and smstools. This month I also sponsored an upload of printrun. After about ten years of living without any power outage, some construction worker decided to cut a cable near my place. Unfortunately one of my computers used for recording TV shows did not boot after the cable had been repaired and I had to switch some timers to other boxes. All in all this was too much stress and I purchased some USVs from APC. As apcupsd was orphaned, I took the opportunity to adopt it as DOPOM for this month. My license pasting project now contains 31 license templates for your debian/copyright. The list of available texts can be obtained with:

curl http://licapi.debian.net/template

The license text itself is available under the given links, for example with

curl http://licapi.debian.net/template/Apache-2

3 November 2017

Rog rio Brito: Comparison of JDK installation of various Linux distributions

Today I spent some time in the morning seeing how one would install the JDK on Linux distributions. This is to create a little comparative tutorial to teach introductory Java. Installing the JDK is, thanks to the OpenJDK developers in Debian and Ubuntu (Matthias Klose and helpers), a very easy task. You simply type something like: 
apt-get install openjdk-8-jdk
Since for a student it is better to have everything for experiments, I install the full version, not only the -headless version. Given my familiarity with Debian/Ubuntu, I didn't have to think about the way of installing it, of course. But as this is a tutorial meant to be as general as I can, I tried also to include instructions on how to install Java on other distributions. The first two that came to my mind were openSUSE and Fedora. Both use the RPM package format for their "native" packages (in the same sense that Debian uses DEB packages for "native" packages). But they use different higher-level tools to install such packages: Fedora uses a tool called dnf, while openSUSE uses zypper. To try these distributions, I got their netinstall ISOs and used qemu/kvm to install on a virtual machine. I used the following to install/run the virtual machines (the example below, is, of course, for openSUSE): 
qemu-system-x86_64 -enable-kvm -m 4096 -smp 2 -net nic,model=e1000 -net user -drive index=0,media=disk,cache=unsafe,file=suse.qcow2 -cdrom openSUSE-Leap-42.3-NET-x86_64.iso
The names of the packages also change from one distribution to another. On Fedora, I had to use: 
dnf install java-1.8.0-openjdk-devel
On openSUSE, I had to use: 
zypper install java-1_8_0-openjdk-devel
Note that one distribution uses dots in the names of the packages while the other uses underscores. One interesting thing that I noticed with dnf was that, when I used it, it automatically refreshed the package lists from the network, something which I forgot, and it was a pleasant surprise. I don't know about zypper, but I guess that it probably had fresh indices when the installation finished. Both installations were effortless after I knew the names of the packages to install. Oh, BTW, in my 5 minute exploration with these distributions, I noticed that if you don't want the JDK, but only the JRE, then you omit the -devel suffix. It makes sense when you think about it, for consistency with other packages, but Debian's conventions also make sense (JRE with -jre suffix, JDK with -jdk suffix). I failed miserably to use Fedora's prebaked, vanilla cloud image, as I couldn't login on this image and I decided to just install the whole OS on a fresh virtual machine. I don't have instructions on how to install on Gentoo nor on Arch, though. I now see how hard it is to cover instructions/provide software for as many distributions as you wish, given the multitude of package managers, conventions etc.

2 November 2017

Antoine Beaupr : October 2017 report: LTS, feed2exec beta, pandoc filters, git mediawiki

Debian Long Term Support (LTS) This is my monthly Debian LTS report. This time I worked on the famous KRACK attack, git-annex, golang and the continuous stream of GraphicsMagick security issues.

WPA & KRACK update I spent most of my time this month on the Linux WPA code, to backport it to the old (~2012) wpa_supplicant release. I first published a patchset based on the patches shipped after the embargo for the oldstable/jessie release. After feedback from the list, I also built packages for i386 and ARM. I have also reviewed the WPA protocol to make sure I understood the implications of the changes required to backport the patches. For example, I removed the patches touching the WNM sleep mode code as that was introduced only in the 2.0 release. Chunks of code regarding state tracking were also not backported as they are part of the state tracking code introduced later, in 3ff3323. Finally, I still have concerns about the nonce setup in patch #5. In the last chunk, you'll notice peer->tk is reset, to_set to negotiate a new TK. The other approach I considered was to backport 1380fcbd9f ("TDLS: Do not modify RNonce for an TPK M1 frame with same INonce") but I figured I would play it safe and not introduce further variations. I should note that I share Matthew Green's observations regarding the opacity of the protocol. Normally, network protocols are freely available and security researchers like me can easily review them. In this case, I would have needed to read the opaque 802.11i-2004 pdf which is behind a TOS wall at the IEEE. I ended up reading up on the IEEE_802.11i-2004 Wikipedia article which gives a simpler view of the protocol. But it's a real problem to see such critical protocols developed behind closed doors like this. At Guido's suggestion, I sent the final patch upstream explaining the concerns I had with the patch. I have not, at the time of writing, received any response from upstream about this, unfortunately. I uploaded the fixed packages as DLA 1150-1 on October 31st.

Git-annex The next big chunk on my list was completing the work on git-annex (CVE-2017-12976) that I started in August. It turns out doing the backport was simpler than I expected, even with my rusty experience with Haskell. Type-checking really helps in doing the right thing, especially considering how Joey Hess implemented the fix: by introducing a new type. So I backported the patch from upstream and notified the security team that the jessie and stretch updates would be similarly easy. I shipped the backport to LTS as DLA-1144-1. I also shared the updated packages for jessie (which required a similar backport) and stretch (which didn't) and those Sebastien Delafond published those as DSA 4010-1.

Graphicsmagick Up next was yet another security vulnerability in the Graphicsmagick stack. This involved the usual deep dive into intricate and sometimes just unreasonable C code to try and fit a round tree in a square sinkhole. I'm always unsure about those patches, but the test suite passes, smoke tests show the vulnerability as fixed, and that's pretty much as good as it gets. The announcement (DLA 1154-1) turned out to be a little special because I had previously noticed that the penultimate announcement (DLA 1130-1) was never sent out. So I made a merged announcement to cover both instead of re-sending the original 3 weeks late, which may have been confusing for our users.

Triage & misc We always do a bit of triage even when not on frontdesk duty, so I: I also did smaller bits of work on: The latter reminded me of the concerns I have about the long-term maintainability of the golang ecosystem: because everything is statically linked, an update to a core library (say the SMTP library as in CVE-2017-15042, thankfully not affecting LTS) requires a full rebuild of all packages including the library in all distributions. So what would be a simple update in a shared library system could mean an explosion of work on statically linked infrastructures. This is a lot of work which can definitely be error-prone: as I've seen in other updates, some packages (for example the Ruby interpreter) just bit-rot on their own and eventually fail to build from source. We would also have to investigate all packages to see which one include the library, something which we are not well equipped for at this point. Wheezy was the first release shipping golang packages but at least it's shipping only one... Stretch has shipped with two golang versions (1.7 and 1.8) which will make maintenance ever harder in the long term.
We build our computers the way we build our cities--over time, without a plan, on top of ruins. - Ellen Ullman

Other free software work This month again, I was busy doing some serious yak shaving operations all over the internet, on top of publishing two of my largest LWN articles to date (2017-10-16-strategies-offline-pgp-key-storage and 2017-10-26-comparison-cryptographic-keycards).

feed2exec beta Since I announced this new project last month I have released it as a beta and it entered Debian. I have also wrote useful plugins like the wayback plugin that saves pages on the Wayback machine for eternal archival. The archive plugin can also similarly save pages to the local filesystem. I also added bash completion, expanded unit tests and documentation, fixed default file paths and a bunch of bugs, and refactored the code. Finally, I also started using two external Python libraries instead of rolling my own code: the pyxdg and requests-file libraries, the latter which I packaged in Debian (and fixed a bug in their test suite). The program is working pretty well for me. The only thing I feel is really missing now is a retry/fail mechanism. Right now, it's a little brittle: any network hiccup will yield an error email, which are readable to me but could be confusing to a new user. Strangely enough, I am particularly having trouble with (local!) DNS resolution that I need to look into, but that is probably unrelated with the software itself. Thankfully, the user can disable those with --loglevel=ERROR to silence WARNINGs. Furthermore, some plugins still have some rough edges. For example, The Transmission integration would probably work better as a distinct plugin instead of a simple exec call, because when it adds new torrents, the output is totally cryptic. That plugin could also leverage more feed parameters to save different files in different locations depending on the feed titles, something would be hard to do safely with the exec plugin now. I am keeping a steady flow of releases. I wish there was a way to see how effective I am at reaching out with this project, but unfortunately GitLab doesn't provide usage statistics... And I have received only a few comments on IRC about the project, so maybe I need to reach out more like it says in the fine manual. Always feels strange to have to promote your project like it's some new bubbly soap... Next steps for the project is a final review of the API and release production-ready 1.0.0. I am also thinking of making a small screencast to show the basic capabilities of the software, maybe with asciinema's upcoming audio support?

Pandoc filters As I mentioned earlier, I dove again in Haskell programming when working on the git-annex security update. But I also have a small Haskell program of my own - a Pandoc filter that I use to convert the HTML articles I publish on LWN.net into a Ikiwiki-compatible markdown version. It turns out the script was still missing a bunch of stuff: image sizes, proper table formatting, etc. I also worked hard on automating more bits of the publishing workflow by extracting the time from the article which allowed me to simply extract the full article into an almost final copy just by specifying the article ID. The only thing left is to add tags, and the article is complete. In the process, I learned about new weird Haskell constructs. Take this code, for example: 
-- remove needless blockquote wrapper around some tables
--
-- haskell newbie tips:
--
-- @ is the "at-pattern", allows us to define both a name for the
-- construct and inspect the contents as once
--
--   is the "empty record pattern": it basically means "match the
-- arguments but ignore the args"
cleanBlock (BlockQuote t@[Table  ]) = t
Here the idea is to remove <blockquote> elements needlessly wrapping a <table>. I can't specify the Table type on its own, because then I couldn't address the table as a whole, only its parts. I could reconstruct the whole table bits by bits, but it wasn't as clean. The other pattern was how to, at last, address multiple string elements, which was difficult because Pandoc treats spaces specially: 
cleanBlock (Plain (Strong (Str "Notifications":Space:Str "for":Space:Str "all":Space:Str "responses":_):_)) = []
The last bit that drove me crazy was the date parsing: 
-- the "GAByline" div has a date, use it to generate the ikiwiki dates
--
-- this is distinct from cleanBlock because we do not want to have to
-- deal with time there: it is only here we need it, and we need to
-- pass it in here because we do not want to mess with IO (time is I/O
-- in haskell) all across the function hierarchy
cleanDates :: ZonedTime -> Block -> [Block]
-- this mouthful is just the way the data comes in from
-- LWN/Pandoc. there could be a cleaner way to represent this,
-- possibly with a record, but this is complicated and obscure enough.
cleanDates time (Div (_, [cls], _)
                 [Para [Str month, Space, Str day, Space, Str year], Para _])
    cls == "GAByline" = ikiwikiRawInline (ikiwikiMetaField "date"
                                           (iso8601Format (parseTimeOrError True defaultTimeLocale "%Y-%B-%e,"
                                                           (year ++ "-" ++ month ++ "-" ++ day) :: ZonedTime)))
                        ++ ikiwikiRawInline (ikiwikiMetaField "updated"
                                             (iso8601Format time))
                        ++ [Para []]
-- other elements just pass through
cleanDates time x = [x]
Now that seems just dirty, but it was even worse before. One thing I find difficult in adapting to coding in Haskell is that you need to take the habit of writing smaller functions. The language is really not well adapted to long discourse: it's more about getting small things connected together. Other languages (e.g. Python) discourage this because there's some overhead in calling functions (10 nanoseconds in my tests, but still), whereas functions are a fundamental and important construction in Haskell that are much more heavily optimized. So I constantly need to remind myself to split things up early, otherwise I can't do anything in Haskell. Other languages are more lenient, which does mean my code can be more dirty, but I feel get things done faster then. The oddity of Haskell makes frustrating to work with. It's like doing construction work but you're not allowed to get the floor dirty. When I build stuff, I don't mind things being dirty: I can cleanup afterwards. This is especially critical when you don't actually know how to make things clean in the first place, as Haskell will simply not let you do that at all. And obviously, I fought with Monads, or, more specifically, "I/O" or IO in this case. Turns out that getting the current time is IO in Haskell: indeed, it's not a "pure" function that will always return the same thing. But this means that I would have had to change the signature of all the functions that touched time to include IO. I eventually moved the time initialization up into main so that I had only one IO function and moved that timestamp downwards as simple argument. That way I could keep the rest of the code clean, which seems to be an acceptable pattern. I would of course be happy to get feedback from my Haskell readers (if any) to see how to improve that code. I am always eager to learn.

Git remote MediaWiki Few people know that there is a MediaWiki remote for Git which allow you to mirror a MediaWiki site as a Git repository. As a disaster recovery mechanism, I have been keeping such a historical backup of the Amateur radio wiki for a while now. This originally started as a homegrown Python script to also convert the contents in Markdown. My theory then was to see if we could switch from Mediawiki to Ikiwiki, but it took so long to implement that I never completed the work. When someone had the weird idea of renaming a page to some impossible long name on the wiki, my script broke. I tried to look at fixing it and then remember I also had a mirror running using the Git remote. It turns out it also broke on the same issue and that got me looking in the remote again. I got lost in a zillion issues, including fixing that specific issue, but I especially looked at the possibility of fetching all namespaces because I realized that the remote fetches only a part of the wiki by default. And that drove me to submit namespace support as a patch to the git mailing list. Finally, the discussion came back to how to actually maintain that contrib: in git core or outside? Finally, it looks like I'll be doing some maintenance that project outside of git, as I was granted access to the GitHub organisation...

Galore Yak Shaving Then there's the usual hodgepodge of fixes and random things I did over the month.
There is no [web extension] only XUL! - Inside joke

1 November 2017

Jonathan Dowland: In defence of "Thought for the Day"

BBC Radio 4's long-running "Thought for the Day" has been in the news this week, as several presenters for the Today Programme have criticised the segment in an interview with Radio Times magazine. One facet of the criticism was whether the BBC should be broadcasting three minutes of religious content daily when more than half of the population are atheist. I'm an atheist and in my day-to-day life I have almost zero interaction with people of faith, certainly none where faith is a topic of conversation. However when I was an undergrad at Durham, I was a member of St John's College which has a Christian/Anglican/Evangelical heritage, and I met a lot of religious friends during my time there. What I find a little disturbing about the lack of faithful people in my day-to-day life, compared to then, is how it shines a light on how disjoint our society is. This has become even more apparent with the advent of the "filter bubble" and how irreconcilable factions are around topics like Brexit, Trump, etc. For these reasons I appreciate Thought for the Day and hearing voices from communities that I normally have little to do with. I can agree with the complaints about the lack of diversity, and I particularly enjoy hearing Thoughts from Muslims, Sikhs, Hindus, Buddhists, and such. Another criticism levelled against the segment was that it can be "preachy". I haven't found that myself. I get the impression that most of the monologues are carefully constructed to be as unpreaching as possible. I can usually appreciate the ethical content of the talks, without having to buy into the faith aspect. Interestingly the current principal of St John's College, David Wilkinson, has written his own response to the interview for the Radio Times.

31 October 2017

Chris Lamb: Free software activities in October 2017

Here is my monthly update covering what I have been doing in the free software world in October 2017 (previous month):
Reproducible builds

Whilst anyone can inspect the source code of free software for malicious flaws, most software is distributed pre-compiled to end users. The motivation behind the Reproducible Builds effort is to allow verification that no flaws have been introduced either maliciously or accidentally during this compilation process by promising identical results are always generated from a given source, thus allowing multiple third-parties to come to a consensus on whether a build was compromised. I have generously been awarded a grant from the Core Infrastructure Initiative to fund my work in this area. This month I:


I also made the following changes to our tooling:
diffoscope

diffoscope is our in-depth and content-aware diff utility that can locate and diagnose reproducibility issues.

  • Improve names in output of "internal" binwalk members. (#877525).
  • Don't crash on malformed md5sums files. (#877473).
  • Omit misleading "any of" prefix when only complaining about a single module on import. [...]
  • Adjust tests as ps2ascii now varies its output on timezone. [...]

strip-nondeterminism

strip-nondeterminism is our tool to remove specific non-deterministic results from a completed build.

  • Clojure considers .class file to be stale if it shares the same timestamp of the .clj. We thus adjust the timestamps of the .clj to always be younger. (#877418).
  • Print a message in --verbose mode if no canonical time was specified. [...]

buildinfo.debian.net

buildinfo.debian.net is my experiment into how to process, store and distribute .buildinfo files after the Debian archive software has processed them.

  • Always show SHA-256 checksums, regardless of the browser viewport size. [...]
  • Add an API endpoint to fetch specific .buildinfo files for a certain package/version/architecture. [...]


Debian My activities as the current Debian Project Leader are covered in my "Bits from the DPL" email to the debian-devel-announce mailing list.
Patches contributed
  • devscripts: Please print the actual arguments debuild makes to Lintian. (#880124)
  • hw-detect: Drop reference to floppy disks; it's almost 2018. (#880122)
  • debci:
    • Use deb.debian.org over http.debian.net. (#879654)
    • Document how to use an alternative mirror. (#879655)
Debian LTS

This month I have been paid to work 18 hours on Debian Long Term Support (LTS). In that time I did the following:
  • "Frontdesk" duties, triaging CVEs, etc.
  • Followed up on a large number of upstream "pings" that have been left dormant.
  • Issued DLA 1121-1 to fix an out-of-bounds read vulnerability in curl where a malicious FTP server could abuse this to prevent clients from interacting with it.
  • Issued DLA 1123-1 for the "Go" programming language where an attacker could generate a MIME request such that the server ran out of file descriptors.
  • Issued DLA 1126-1 for the libxfont font selection and rasterisation library, correcting two vulnerabilities, both involving the library being tricked into reading invalid/random memory.
  • Issued DLA 1134-1 for sdl-image1.2, an image loading library. A maliciously-crafted .xcf file could cause a stack-based buffer overflow resulting in potential code execution.
Uploads
  • python-django:
    • 2.0~beta1-1 New upstream 2.x release.
    • 1.11.6-1 New upstream bugfix release.
  • gunicorn (19.6.0-10+deb9u1) Prepared a release for stable to avoid a runtime dependency on a compiler. (#877722)
  • redis:
    • 4:4.0.2-3:
      • Drop the Debian-specific /etc/redis/redis-server.pre-up.d (etc.) hooks and remove them if unchanged.
      • Include systemd redis-server@.service and redis-sentinel@.service template files to easily run multiple Redis instances. (#877702)
      • Patch redis.conf and sentinel.conf with quilt instead of maintaining our own versions under debian/.
    • 4:4.0.2-4:
      • Add input validity checking to cluster config slot numbers to fix CVE-2017-15047. (#878076)
      • Drop debian/bin/generate-parts now we aren't calling it.
      • Correct Bash-ism in NEWS file.
    • 4:4.0.2-5: Replace the existing patch for CVE-2017-15047 with an upstream-blessed version that covers another case.
  • redisearch (0.21.3-5) Initial release.
  • docbook2man (2.0.0-40) Correct spelling mistakes in binaries and other misc packaging tidying.
  • python-redis (2.10.6-1) New upstream release.
  • bfs (1.1.3-1) New upstream release.
FTP Team

As a Debian FTP assistant I ACCEPTed 103 packages: amcheck, argagg, binutils, blockui, bro-pkg, chkservice, citus, django-axes, docker-containerd, doctest, dtkwidget, duktape, feed2exec, fontforge, fonttools, gcc-8, gcc-8-cross, generator-scripting-language, gitgraph.js, haskell-uri-encode, hoel, iniparser, its, jquery-areyousure, kodi, libcatmandu-mods-perl, libcatmandu-template-perl, libcatmandu-xml-perl, libcatmandu-xsd-perl, libcode-tidyall-plugin-sortlines-naturally-perl, libgdamm5.0, libinfinity, libmods-record-perl, libreoffice-dictionaries, libset-intervaltree-perl, libsodium, linux, linux-grsec, ltsp-manager, lxqt-themes, mailman3-core, measurement-kit, mini-buildd, musescore, node-babel, node-babel-eslint, node-babel-loader, node-babel-plugin-add-module-exports, node-babel-plugin-transform-define, node-gulp-newer, node-regenerate-unicode-properties, node-regexpu-core, node-regjsparser, node-unicode-data, node-unicode-loose-match, openjdk-9, orafce, pgaudit, pgsql-ogr-fdw, pk4, postgresql-mysql-fdw, powa-archivist, python-azure-devtools, python-colormap, python-darkslide, python-dotenv, python-karborclient, python-logfury, python-lupa, python-marshmallow, python-murano-pkg-check, python-octaviaclient, python-pathspec, python-pgpy, python-pydub, python-randomize, python-sabyenc, python-searchlightclient, python-stestr, python-subunit2sql, python-twitter, python-utils, python-wsgilog, r-cran-bindr, r-cran-desc, r-cran-hms, r-cran-readstata13, r-cran-rprojroot, r-cran-wikidatar, r-cran-wikipedir, r-cran-wikitaxa, repmgr, requests-file, resteasy3.0, sdl-kitchensink, stardicter, systemd-el, thunderbird, tomcat8.0, uwsgi-plugin-luajit, uwsgi-plugin-mongo, uwsgi-plugin-php & uwsgi-plugin-v8. I additionally filed 3 RC bugs against packages that had incomplete debian/copyright files against: fonttools, generator-scripting-language & libsodium.

Dirk Eddelbuettel: linl 0.0.2: Couple improvements

Following up on the initial 0.0.1 release of linl, Aaron and I are happy to announce release 0.0.2 which reached the CRAN network on Sunday in a smooth 'CRAN-pretest-publish' auto-admittance. linl provides a simple-yet-powerful Markdown---and RMarkdown---wrapper around the venerable LaTeX letter class; see below for an expanded example also included as the package vignette. This versions sets a few sensible default values for font, font size, margins, signature (non-)indentation and more; it also expands the documentation.
The NEWS entry follows:

Changes in tint version 0.0.2 (2017-10-29)
  • Set a few defaults for a decent-looking skeleton and template: font, fontsize, margins, left-justify closing (#3)
  • Blockquote display is now a default as well (#4).
  • Updated skeleton.Rmd and vignette source accordingly
  • Documented new default options (#5 and #6).
  • Links are now by default printed as footnotes (#9).

Courtesy of CRANberries, there is a comparison to the previous release. More information is on the tint page. For questions or comments use the issue tracker off the GitHub repo. For questions or comments use the issue tracker off the GitHub repo.

This post by Dirk Eddelbuettel originated on his Thinking inside the box blog. Please report excessive re-aggregation in third-party for-profit settings.

Norbert Preining: Debian/TeX Live 2017.20171031-1

Halloween is here, time to upload a new set of scary packages of TeX Live. About a month has passed, so there is the usual big stream up updates. There was actually an intermediate release to get out some urgent fixes, but I never reported the news here. So here are the accumulated changes and updates. My favorite this time is wallcalendar, a great class to design all kind of calendars, it looks really well done. I immediately will start putting one together. On the font side there is the new addition coelacanth. To quote from the README: Coelacanth is inspired by the classic Centaur type design of Bruce Rogers, described by some as the most beautiful typeface ever designed. It aims to be a professional quality type family for general book typesetting. And indeed it is beautiful! Other noteworthy addition is the Spark font that allows creating sparklines in the running text with LaTeX. Enjoy. New packages algobox, amscls-doc, beilstein, bib2gls, coelacanth, crossreftools, dejavu-otf, dijkstra, ducksay, dynkin-diagrams, eqnnumwarn, fetchcls, fixjfm, glossaries-finnish, hagenberg-thesis, hecthese, ifxptex, isopt, istgame, ku-template, limecv, mensa-tex, musicography, na-position, notestex, outlining, pdfreview, spark-otf, spark-otf-fonts, theatre, unitn-bimrep, upzhkinsoku, wallcalendar, xltabular. Updated packages acmart, amsmath, animate, arabluatex, arara, babel, babel-french, bangorexam, baskervillef, beebe, biblatex-philosophy, biblatex-source-division, bibletext, bidi, bxjaprnind, bxjscls, bxpapersize, bytefield, classicthesis, cochineal, complexity, cooking-units, curves, datetime2-german, dccpaper, doclicense, docsurvey, eledmac, epstopdf, eqparbox, esami, etoc, fbb, fei, fithesis, fmtcount, fnspe, fonts-tlwg, fontspec, genealogytree, glossaries, glossaries-extra, hecthese, hepthesis, hvfloat, ifplatform, ifptex, inconsolata, jfmutil, jsclasses, ketcindy, knowledge, koma-script, l3build, l3experimental, l3kernel, l3packages, langsci, latex2man, latexbug, lato, leadsheets, libertinust1math, listofitems, luatexja, luatexko, luatodonotes, lwarp, markdown, mcf2graph, media9, newtx, novel, numspell, ocgx2, overpic, philokalia, phonenumbers, platex, poemscol, pst-exa, pst-geometrictools, pst-ovl, pst-plot, pst-pulley, pst-tools, pst-vehicle, pst2pdf, pstool, pstricks, pstricks-add, pxchfon, pxjahyper, quran, randomlist, rec-thy, reledmac, robustindex, scratch, skrapport, spectralsequences, tcolorbox, tetex, tex4ht, texcount, texdoc, tikzducks, tikzsymbols, toptesi, translation-biblatex-de, unicode-math, updmap-map, uplatex, widetable, xcharter, xepersian, xetexko, xetexref, xsim, zhlipsum.

26 October 2017

Russell Coker: Anarchy in the Office

Some of the best examples I ve seen of anarchy working have been in corporate environments. This doesn t mean that they were perfect or even as good as a theoretical system in which a competent manager controlled everything, but they often worked reasonably well. In a well functioning team members will encourage others to do their share of the work in the absence of management. So when the manager disappears (doesn t visit the team more than once a week and doesn t ask for any meaningful feedback on how things are going) things can still work out. When someone who is capable of doing work isn t working then other people will suggest that they do their share. If resources for work (such as a sufficiently configured PC for IT work) aren t available then they can be found (abandoned PCs get stripped and the parts used to upgrade the PCs that need it most). There was one time where a helpdesk worker who was about to be laid off was assigned to the same office as me (apparently making all the people in his group redundant took some time). So I started teaching him sysadmin skills, assigned work to him, and then recommended that my manager get him transferred to my group. That worked well for everyone. One difficult case is employees who get in the way of work being done, those who are so incompetent that they break enough things to give negative productivity. One time when I was working in Amsterdam I had two colleagues like that, it turned out that the company had no problem with employees viewing porn at work so no-one asked them to stop looking at porn. Having them paid to look at porn 40 hours a week was much better than having them try to do work. With anarchy there s little option to get rid of bad people, so just having them hang out and do no work was the only option. I m not advocating porn at work (it makes for a hostile work environment), but managers at that company did worse things. One company I worked for appeared (from the non-management perspective) to have a management culture of doing no work. During my time there I did two annual reviews in two weeks, and the second was delayed by over 6 months. The manager in question only did the reviews at that time because he was told he couldn t be promoted until he got the backlog of reviews done, so apparently being more than a year behind in annual reviews was no obstacle to being selected for promotion. On one occasion I raised the issue of a colleague who had done no work for over a year (and didn t even have a PC to do work) with that manager, his response was what do you expect me to do ! I expected him to do anything other than blow me off when I reported such a serious problem! But in spite of that strictly work-optional culture enough work was done and the company was a leader in it s field. There has been a lot of research into the supposed benefits of bonuses etc which usually turn out to reduce productivity. Such research is generally ignored presumably because the people who are paid the most are the ones who get to decide whether financial incentives should be offered so they choose the compensation model for the company that benefits themselves. But the fact that teams can be reasonably productive when some people are paid to do nothing and most people have their work allocated by group consensus rather than management plan seems to be a better argument against the typical corporate management. I think it would be interesting to try to run a company with an explicit anarchic management and see how it compares to the accidental anarchy that so many companies have. The idea would be to have minimal management that just does the basic HR tasks (preventing situations of bullying etc), a flat pay rate for everyone (no bonuses, pay rises, etc) and have workers decide how to spend money for training, facilities, etc. Instead of having middle managers you would have representatives elected from each team to represent their group to senior management. PS Australia has some of the strictest libel laws in the world. Comments that identify companies or people are likely to be edited or deleted.
Related posts:
  1. Preferring Not To I ve just read Bartleby the Scrivener which is a short...
  2. Contract Pay Rates In a comment on my post about Bad Project Management...
  3. more about securing an office My post about securing an office received many comments, so...

24 October 2017

Iain R. Learmonth: Security by Obscurity

Today this blog post turned up on Hacker News, titled Obscurity is a Valid Security Layer . It makes some excellent points on the distinction between good and bad obscurity and it gives an example of good obscurity with SSH. From the post:
I configured my SSH daemon to listen on port 24 in addition to its regular port of 22 so I could see the difference in attempts to connect to each (the connections are usually password guessing attempts). My expected result is far fewer attempts to access SSH on port 24 than port 22, which I equate to less risk to my, or any, SSH daemon. I ran with this alternate port configuration for a single weekend, and received over eighteen thousand (18,000) connections to port 22, and five (5) to port 24.
Those of you that know me in the outside world will have probably heard me talk about how it s insane we have all these services running on the public Internet that don t need to be there, just waiting to be attacked. I have previously given a talk at TechMeetup Aberdeen where I talk about my use of Tor s Onion services to have services that only I should ever connect to be hidden from the general Internet. Onion services, especially the client authentication features, can also be useful for IoT dashboards and devices, allowing access from the Internet but via a secure and authenticated channel that is updated even when the IoT devices behind it have long been abandoned. If you re interested to learn more about Onion services, you could watch Roger Dingledine s talk from Def Con 25.

23 October 2017

Russ Allbery: Review: Algorithms to Live By

Review: Algorithms to Live By, by Brian Christian & Tom Griffiths
Publisher: Henry Holt and Company
Copyright: April 2016
ISBN: 1-62779-037-3
Format: Kindle
Pages: 255
Another read for the work book club. This was my favorite to date, apart from the books I recommended myself. One of the foundations of computer science as a field of study is research into algorithms: how do we solve problems efficiently using computer programs? This is a largely mathematical field, but it's often less about ideal or theoretical solutions and more about making the most efficient use of limited resources and arriving at an adequate, if not perfect, answer. Many of these problems are either day-to-day human problems or are closely related to them; after all, the purpose of computer science is to solve practical problems with computers. The question asked by Algorithms to Live By is "can we reverse this?": can we learn lessons from computer science's approach to problems that would help us make day-to-day decisions? There's a lot of interesting material in the eleven chapters of this book, but there's also an amusing theme: humans are already very good at this. Many chapters start with an examination of algorithms and mathematical analysis of problems, dive into a discussion of how we can use those results to make better decisions, then talk about studies of the decisions humans actually make... and discover that humans are already applying ad hoc versions of the best algorithms we've come up with, given the constraints of typical life situations. It tends to undermine the stated goal of the book. Thankfully, it in no way undermines interesting discussion of general classes of problems, how computer science has tackled them, and what we've learned about the mathematical and technical shapes of those problems. There's a bit less self-help utility here than I think the authors had intended, but lots of food for thought. (That said, it's worth considering whether this congruence is less because humans are already good at this and more because our algorithms are designed from human intuition. Maybe our best algorithms just reflect human thinking. In some cases we've checked our solutions against mathematical ideals, but in other cases they're still just our best guesses to date.) This is the sort of a book where a chapter listing is an important part of the review. The areas of algorithms discussed here are optimal stopping, explore/exploit decisions (when to go with the best thing you've found and when to look for something better), sorting, caching, scheduling, Bayes's rule (and prediction in general), overfitting when building models, relaxation (solving an easier problem than your actual problem), randomized algorithms, a collection of networking algorithms, and finally game theory. Each of these has useful insights and thought-provoking discussion of how these sometimes-theoretical concepts map surprisingly well onto daily problems. The book concludes with a discussion of "computational kindness": an encouragement to reduce the required computation and complexity penalty for both yourself and the people you interact with. If you have a computer science background (as I do), many of these will be familiar concepts, and you might be dubious that a popularization would tell you much that's new. Give this book a shot, though; the analogies are less stretched than you might fear, and the authors are both careful and smart about how they apply these principles. This book passes with flying colors a key sanity check: the chapters on topics that I know well or have thought about a lot make few or no obvious errors and say useful and important things. For example, the scheduling chapter, which unsurprisingly is about time management, surpasses more than half of the time management literature by jumping straight to the heart of most time management problems: if you're going to do everything on a list, it rarely matters the order in which you do it, so the hardest scheduling problems are about deciding what not to do rather than deciding order. The point in the book where the authors won my heart completely was in the chapter on Bayes's rule. Much of the chapter is about Bayesian priors, and how one's knowledge of past events is a vital part of analysis of future probabilities. The authors then discuss the (in)famous marshmallow experiment, in which children are given one marshmallow and told that if they refrain from eating it until the researcher returns, they'll get two marshmallows. Refraining from eating the marshmallow (delayed gratification, in the psychological literature) was found to be associated with better life outcomes years down the road. This experiment has been used and abused for years for all sorts of propaganda about how trading immediate pleasure for future gains leads to a successful life, and how failure in life is because of inability to delay gratification. More evil analyses have (of course) tied that capability to ethnicity, with predictably racist results. I have kind of a thing about the marshmallow experiment. It's a topic that reliably sends me off into angry rants. Algorithms to Live By is the only book I have ever read to mention the marshmallow experiment and then apply the analysis that I find far more convincing. This is not a test of innate capability in the children; it's a test of their Bayesian priors. When does it make perfect sense to eat the marshmallow immediately instead of waiting for a reward? When their past experience tells them that adults are unreliable, can't be trusted, disappear for unpredictable lengths of time, and lie. And, even better, the authors supported this analysis with both a follow-up study I hadn't heard of before and with the observation that some children would wait for some time and then "give in." This makes perfect sense if they were subconsciously using a Bayesian model with poor priors. This is a great book. It may try a bit too hard in places (applicability of the math of optimal stopping to everyday life is more contingent and strained than I think the authors want to admit), and some of this will be familiar if you've studied algorithms. But the writing is clear, succinct, and very well-edited. No part of the book outlives its welcome; the discussion moves right along. If you find yourself going "I know all this already," you'll still probably encounter a new concept or neat explanation in a few more pages. And sometimes the authors make connections that never would have occurred to me but feel right in retrospect, such as relating exponential backoff in networking protocols to choosing punishments in the criminal justice system. Or the realization that our modern communication world is not constantly connected, it's constantly buffered, and many of us are suffering from the characteristic signs of buffer bloat. I don't think you have to be a CS major, or know much about math, to read this book. There is a lot of mathematical details in the end notes if you want to dive in, but the main text is almost always readable and clear, at least so far as I could tell (as someone who was a CS major and has taken a lot of math, so a grain of salt may be indicated). And it still has a lot to offer even if you've studied algorithms for years. The more I read of this book, the more I liked it. Definitely recommended if you like reading this sort of analysis of life. Rating: 9 out of 10

18 October 2017

Joey Hess: extending Scuttlebutt with Annah

This post has it all. Flotillas of sailboats, peer-to-peer wikis, games, and de-frogging. But, I need to start by talking about some tech you may not have heard of yet... So, how could these be combined together, and what might the result look like? Well, I could start by posting a Scuttlebutt message that defines what True is. And another Scuttlebutt message defining False. And then, another Scuttlebutt message to define the AND function, which would link to my messages for True and False. Continue this until I've built up enough Annah code to write some almost useful programs. Annah can't do any IO on its own (though it can model IO similarly to how Haskell does), so for programs to be actually useful, there needs to be Scuttlebutt client support. The way typing works in Annah, a program's type can be expressed as a Scuttlebutt link. So a Scuttlebutt client that wants to run Annah programs of a particular type can pick out programs that link to that type, and will know what type of data the program consumes and produces. Here are a few ideas of what could be built, with fairly simple client-side support for different types of Annah programs... This kind of extensibility in a peer-to-peer system is exciting! With these new systems, we can consider lessons from the world wide web and replicate some of the good parts, while avoiding the bad. Javascript has been both good and bad for the web. The extensibility is great, and yet it's a neverending security and privacy nightmare, and it ties web pages ever more tightly to programs hidden away on servers. I believe that Annah combined with Scuttlebutt will comprehensively avoid those problems. Shall we build it?
This exploration was sponsored by Jake Vosloo on Patreon.

17 October 2017

Reproducible builds folks: Reproducible Builds: Weekly report #129

Here's what happened in the Reproducible Builds effort between Sunday October 8 and Saturday October 14 2017: Upcoming events Reproducible work in other projects Pierre Pronchery reported that that he has built the foundations for doing more reproducibility work in NetBSD. Packages fixed Upstream bugs and patches: Reproducibility non-maintainer uploads in Debian: QA fixes in Debian: Reviews of unreproducible packages 6 package reviews have been added, 30 have been updated and 37 have been removed in this week, adding to our knowledge about identified issues. Weekly QA work During our reproducibility testing, FTBFS bugs have been detected and reported by: diffoscope development reprotest development Version 0.7.3 was uploaded to unstable by Ximin Luo. It included contributions already covered by posts of the previous weeks, as well as new ones: Misc. This week's edition was written by Ximin Luo, Chris Lamb and Holger Levsen & reviewed by a bunch of Reproducible Builds folks on IRC & the mailing lists.

Norbert Preining: Japanese TeX User Meeting 2017

Last saturday the Japanese TeX User Meeting took place in Fujisawa, Kanagawa. For those who have been at the TUG 2013 in Tokyo you will remember that the Japanese TeX community is quite big and vibrant. On Saturday about 50 users and developers gathered for a set of talks on a variety of topics. The first talk was by Keiichiro Shikano ( ) on using Markup text to generate (La)TeX and HTML. He presented a variety of markup formats, including his own tool xml2tex. The second talk was my Masamichi Hosoda ( ) on reducing the size of PDF files using PDFmark extraction. As a contributor to many projects including Texinfo and LilyPond, Masamichi Hosoda tells us horror stories about multiple font embedding in the manual of LilyPond, the permanent need for adaption to newer Ghostscript versions, and the very recent development in Ghostscript prohibiting the merge of font definitions in PDF files. Next up was Yusuke Terada ( ) on grading exams using TeX. Working through hundreds and hundreds of exams and do the grading is something many of us are used to and I think nobody really enjoys it. Yusuke Terada has combined various tools, including scans, pdf merging using pdfpages, to generate gradable PDF which were then checked on an iPad. On the way he did hit some limits in dvipdfmx on the number of images, but this was obviously only a small bump on the road. Now if that could be automatized as a nice application, it would be a big hit I guess! The forth talk was by Satoshi Yamashita ( ) on the preparation of slides using KETpic. KETpic is a long running project by Setsuo Takato ( ) for the generation of graphics, in particular using Cinderella. KETpic and KETcindy integrates with lots of algebraic and statistical programs (R, Maxima, SciLab, ) and has a long history of development. Currently there are activities to incorporate it into TeX Live. The fifth talk was by Takuto Asakura ( ) on programming TeX using expl3, the main building block of the LaTeX3 project and already adopted by many TeX developers. Takuto Asakura came to fame on this years TUG/BachoTeX 2017 when he won the W. J. Martin Prize for his presentation Implementing bioinformatics algorithms in TeX. I think we can expect great new developments from Takuto! The last talk was by myself on fmtutil and updmap, two of the main management programs in any TeX installation, presenting the changes introduced over the last year, including the most recent release of TeX Live. Details have been posted on my blog, and a lengthy article in TUGboat 38:2, 2017 is available on this topic, too. After the conference about half of the participants joined a social dinner in a nearby Izakaya, followed by a after-dinner beer tasting at a local craft beer place. Thanks to Tatsuyoshi Hamada for the organization. As usual, the Japanese TeX User Meetings are a great opportunity to discuss new features and make new friends. I am always grateful to be part of this very nice community! I am looking forward to the next year s meeting.

Antoine Beaupr : A comparison of cryptographic keycards

An earlier article showed that private key storage is an important problem to solve in any cryptographic system and established keycards as a good way to store private key material offline. But which keycard should we use? This article examines the form factor, openness, and performance of four keycards to try to help readers choose the one that will fit their needs. I have personally been using a YubiKey NEO, since a 2015 announcement on GitHub promoting two-factor authentication. I was also able to hook up my SSH authentication key into the YubiKey's 2048 bit RSA slot. It seemed natural to move the other subkeys onto the keycard, provided that performance was sufficient. The mail client that I use, (Notmuch), blocks when decrypting messages, which could be a serious problems on large email threads from encrypted mailing lists. So I built a test harness and got access to some more keycards: I bought a FST-01 from its creator, Yutaka Niibe, at the last DebConf and Nitrokey donated a Nitrokey Pro. I also bought a YubiKey 4 when I got the NEO. There are of course other keycards out there, but those are the ones I could get my hands on. You'll notice none of those keycards have a physical keypad to enter passwords, so they are all vulnerable to keyloggers that could extract the key's PIN. Keep in mind, however, that even with the PIN, an attacker could only ask the keycard to decrypt or sign material but not extract the key that is protected by the card's firmware.

Form factor The Nitrokey Pro, YubiKey NEO (worn out), YubiKey 4, and FST-01 The four keycards have similar form factors: they all connect to a standard USB port, although both YubiKey keycards have a capacitive button by which the user triggers two-factor authentication and the YubiKey 4 can also require a button press to confirm private key use. The YubiKeys feel sturdier than the other two. The NEO has withstood two years of punishment in my pockets along with the rest of my "real" keyring and there is only minimal wear on the keycard in the picture. It's also thinner so it fits well on the keyring. The FST-01 stands out from the other two with its minimal design. Out of the box, the FST-01 comes without a case, so the circuitry is exposed. This is deliberate: one of its goals is to be as transparent as possible, both in terms of software and hardware design and you definitely get that feeling at the physical level. Unfortunately, that does mean it feels more brittle than other models: I wouldn't carry it in my pocket all the time, although there is a case that may protect the key a little better, but it does not provide an easy way to hook it into a keyring. In the group picture above, the FST-01 is the pink plastic thing, which is a rubbery casing I received along with the device when I got it. Notice how the USB connectors of the YubiKeys differ from the other two: while the FST-01 and the Nitrokey have standard USB connectors, the YubiKey has only a "half-connector", which is what makes it thinner than the other two. The "Nano" form factor takes this even further and almost disappears in the USB port. Unfortunately, this arrangement means the YubiKey NEO often comes loose and falls out of the USB port, especially when connected to a laptop. On my workstation, however, it usually stays put even with my whole keyring hanging off of it. I suspect this adds more strain to the host's USB port but that's a tradeoff I've lived with without any noticeable wear so far. Finally, the NEO has this peculiar feature of supporting NFC for certain operations, as LWN previously covered, but I haven't used that feature yet. The Nitrokey Pro looks like a normal USB key, in contrast with the other two devices. It does feel a little brittle when compared with the YubiKey, although only time will tell how much of a beating it can take. It has a small ring in the case so it is possible to carry it directly on your keyring, but I would be worried the cap would come off eventually. Nitrokey devices are also two times thicker than the Yubico models which makes them less convenient to carry around on keyrings.

Open and closed designs The FST-01 is as open as hardware comes, down to the PCB design available as KiCad files in this Git repository. The software running on the card is the Gnuk firmware that implements the OpenPGP card protocol, but you can also get it with firmware implementing a true random number generator (TRNG) called NeuG (pronounced "noisy"); the device is programmable through a standard Serial Wire Debug (SWD) port. The Nitrokey Start model also runs the Gnuk firmware. However, the Nitrokey website announces only ECC and RSA 2048-bit support for the Start, while the FST-01 also supports RSA-4096. Nitrokey's founder Jan Suhr, in a private email, explained that this is because "Gnuk doesn't support RSA-3072 or larger at a reasonable speed". Its devices (the Pro, Start, and HSM models) use a similar chip to the FST-01: the STM32F103 microcontroller. Nitrokey Pro with STM32F103TBU6 MCU Nitrokey also publishes its hardware designs, on GitHub, which shows the Pro is basically a fork of the FST-01, according to the ChangeLog. I opened the case to confirm it was using the STM MCU, something I should warn you against; I broke one of the pins holding it together when opening it so now it's even more fragile. But at least, I was able to confirm it was built using the STM32F103TBU6 MCU, like the FST-01. Nitrokey back side But this is where the comparison ends: on the back side, we find a SIM card reader that holds the OpenPGP card that, in turn, holds the private key material and does the cryptographic operations. So, in effect, the Nitrokey Pro is really a evolution of the original OpenPGP card readers. Nitrokey confirmed the OpenPGP card featured in the Pro is the same as the one shipped by the Free Software Foundation Europe (FSFE): the BasicCard built by ZeitControl. Those cards, however, are covered by NDAs and the firmware is only partially open source. This makes the Nitrokey Pro less open than the FST-01, but that's an inevitable tradeoff when choosing a design based on the OpenPGP cards, which Suhr described to me as "pretty proprietary". There are other keycards out there, however, for example the SLJ52GDL150-150k smartcard suggested by Debian developer Yves-Alexis Perez, which he prefers as it is certified by French and German authorities. In that blog post, he also said he was experimenting with the GPL-licensed OpenPGP applet implemented by the French ANSSI. But the YubiKey devices are even further away in the closed-design direction. Both the hardware designs and firmware are proprietary. The YubiKey NEO, for example, cannot be upgraded at all, even though it is based on an open firmware. According to Yubico's FAQ, this is due to "best security practices": "There is a 'no upgrade' policy for our devices since nothing, including malware, can write to the firmware." I find this decision questionable in a context where security updates are often more important than trying to design a bulletproof design, which may simply be impossible. And the YubiKey NEO did suffer from critical security issue that allowed attackers to bypass the PIN protection on the card, which raises the question of the actual protection of the private key material on those cards. According to Niibe, "some OpenPGP cards store the private key unencrypted. It is a common attitude for many smartcard implementations", which was confirmed by Suhr: "the private key is protected by hardware mechanisms which prevent its extraction and misuse". He is referring to the use of tamper resistance. After that security issue, there was no other option for YubiKey NEO users than to get a new keycard (for free, thankfully) from Yubico, which also meant discarding the private key material on the key. For OpenPGP keys, this may mean having to bootstrap the web of trust from scratch if the keycard was responsible for the main certification key. But at least the NEO is running free software based on the OpenPGP card applet and the source is still available on GitHub. The YubiKey 4, on the other hand, is now closed source, which was controversial when the new model was announced last year. It led the main Linux Foundation system administrator, Konstantin Ryabitsev, to withdraw his endorsement of Yubico products. In response, Yubico argued that this approach was essential to the security of its devices, which are now based on "a secure chip, which has built-in countermeasures to mitigate a long list of attacks". In particular, it claims that:
A commercial-grade AVR or ARM controller is unfit to be used in a security product. In most cases, these controllers are easy to attack, from breaking in via a debug/JTAG/TAP port to probing memory contents. Various forms of fault injection and side-channel analysis are possible, sometimes allowing for a complete key recovery in a shockingly short period of time.
While I understand those concerns, they eventually come down to the trust you have in an organization. Not only do we have to trust Yubico, but also hardware manufacturers and designs they have chosen. Every step in the hidden supply chain is then trusted to make correct technical decisions and not introduce any backdoors. History, unfortunately, is not on Yubico's side: Snowden revealed the example of RSA security accepting what renowned cryptographer Bruce Schneier described as a "bribe" from the NSA to weaken its ECC implementation, by using the presumably backdoored Dual_EC_DRBG algorithm. What makes Yubico or its suppliers so different from RSA Security? Remember that RSA Security used to be an adamant opponent to the degradation of encryption standards, campaigning against the Clipper chip in the first crypto wars. Even if we trust the Yubico supply chain, how can we trust a closed design using what basically amounts to security through obscurity? Publicly auditable designs are an important tradition in cryptography, and that principle shouldn't stop when software is frozen into silicon. In fact, a critical vulnerability called ROCA disclosed recently affects closed "smartcards" like the YubiKey 4 and allows full private key recovery from the public key if the key was generated on a vulnerable keycard. When speaking with Ars Technica, the researchers outlined the importance of open designs and questioned the reliability of certification:
Our work highlights the dangers of keeping the design secret and the implementation closed-source, even if both are thoroughly analyzed and certified by experts. The lack of public information causes a delay in the discovery of flaws (and hinders the process of checking for them), thereby increasing the number of already deployed and affected devices at the time of detection.
This issue with open hardware designs seems to be recurring topic of conversation on the Gnuk mailing list. For example, there was a discussion in September 2017 regarding possible hardware vulnerabilities in the STM MCU that would allow extraction of encrypted key material from the key. Niibe referred to a talk presented at the WOOT 17 workshop, where Johannes Obermaier and Stefan Tatschner, from the Fraunhofer Institute, demonstrated attacks against the STMF0 family MCUs. It is still unclear if those attacks also apply to the older STMF1 design used in the FST-01, however. Furthermore, extracted private key material is still protected by user passphrase, but the Gnuk uses a weak key derivation function, so brute-forcing attacks may be possible. Fortunately, there is work in progress to make GnuPG hash the passphrase before sending it to the keycard, which should make such attacks harder if not completely pointless. When asked about the Yubico claims in a private email, Niibe did recognize that "it is true that there are more weak points in general purpose implementations than special implementations". During the last DebConf in Montreal, Niibe explained:
If you don't trust me, you should not buy from me. Source code availability is only a single factor: someone can maliciously replace the firmware to enable advanced attacks.
Niibe recommends to "build the firmware yourself", also saying the design of the FST-01 uses normal hardware that "everyone can replicate". Those advantages are hard to deny for a cryptographic system: using more generic components makes it harder for hostile parties to mount targeted attacks. A counter-argument here is that it can be difficult for a regular user to audit such designs, let alone physically build the device from scratch but, in a mailing list discussion, Debian developer Ian Jackson explained that:
You don't need to be able to validate it personally. The thing spooks most hate is discovery. Backdooring supposedly-free hardware is harder (more costly) because it comes with greater risk of discovery. To put it concretely: if they backdoor all of them, someone (not necessarily you) might notice. (Backdooring only yours involves messing with the shipping arrangements and so on, and supposes that you specifically are of interest.)
Since that, as far as we know, the STM microcontrollers are not backdoored, I would tend to favor those devices instead of proprietary ones, as such a backdoor would be more easily detectable than in a closed design. Even though physical attacks may be possible against those microcontrollers, in the end, if an attacker has physical access to a keycard, I consider the key compromised, even if it has the best chip on the market. In our email exchange, Niibe argued that "when a token is lost, it is better to revoke keys, even if the token is considered secure enough". So like any other device, physical compromise of tokens may mean compromise of the key and should trigger key-revocation procedures.

Algorithms and performance To establish reliable performance results, I wrote a benchmark program naively called crypto-bench that could produce comparable results between the different keys. The program takes each algorithm/keycard combination and runs 1000 decryptions of a 16-byte file (one AES-128 block) using GnuPG, after priming it to get the password cached. I assume the overhead of GnuPG calls to be negligible, as it should be the same across all tokens, so comparisons are possible. AES encryption is constant across all tests as it is always performed on the host and fast enough to be irrelevant in the tests. I used the following:
  • Intel(R) Core(TM) i3-6100U CPU @ 2.30GHz running Debian 9 ("stretch"/stable amd64), using GnuPG 2.1.18-6 (from the stable Debian package)
  • Nitrokey Pro 0.8 (latest firmware)
  • FST-01, running Gnuk version 1.2.5 (latest firmware)
  • YubiKey NEO OpenPGP applet 1.0.10 (not upgradable)
  • YubiKey 4 4.2.6 (not upgradable)
I ran crypto-bench for each keycard, which resulted in the following:
Algorithm Device Mean time (s)
ECDH-Curve25519 CPU 0.036
FST-01 0.135
RSA-2048 CPU 0.016
YubiKey-4 0.162
Nitrokey-Pro 0.610
YubiKey-NEO 0.736
FST-01 1.265
RSA-4096 CPU 0.043
YubiKey-4 0.875
Nitrokey-Pro 3.150
FST-01 8.218
Decryption graph There we see the performance of the four keycards I tested, compared with the same operations done without a keycard: the "CPU" device. That provides the baseline time of GnuPG decrypting the file. The first obvious observation is that using a keycard is slower: in the best scenario (FST-01 + ECC) we see a four-fold slowdown, but in the worst case (also FST-01, but RSA-4096), we see a catastrophic 200-fold slowdown. When I presented the results on the Gnuk mailing list, GnuPG developer Werner Koch confirmed those "numbers are as expected":
With a crypto chip RSA is much faster. By design the Gnuk can't be as fast - it is just a simple MCU. However, using Curve25519 Gnuk is really fast.
And yes, the FST-01 is really fast at doing ECC, but it's also the only keycard that handles ECC in my tests; the Nitrokey Start and Nitrokey HSM should support it as well, but I haven't been able to test those devices. Also note that the YubiKey NEO doesn't support RSA-4096 at all, so we can only compare RSA-2048 across keycards. We should note, however, that ECC is slower than RSA on the CPU, which suggests the Gnuk ECC implementation used by the FST-01 is exceptionally fast. In discussions about improving the performance of the FST-01, Niibe estimated the user tolerance threshold to be "2 seconds decryption time". In a new design using the STM32L432 microcontroller, Aurelien Jarno was able to bring the numbers for RSA-2048 decryption from 1.27s down to 0.65s, and for RSA-4096, from 8.22s down to 3.87s seconds. RSA-4096 is still beyond the two-second threshold, but at least it brings the FST-01 close to the YubiKey NEO and Nitrokey Pro performance levels. We should also underline the superior performance of the YubiKey 4: whatever that thing is doing, it's doing it faster than anyone else. It does RSA-4096 faster than the FST-01 does RSA-2048, and almost as fast as the Nitrokey Pro does RSA-2048. We should also note that the Nitrokey Pro also fails to cross the two-second threshold for RSA-4096 decryption. For me, the FST-01's stellar performance with ECC outshines the other devices. Maybe it says more about the efficiency of the algorithm than the FST-01 or Gnuk's design, but it's definitely an interesting avenue for people who want to deploy those modern algorithms. So, in terms of performance, it is clear that both the YubiKey 4 and the FST-01 take the prize in their own areas (RSA and ECC, respectively).

Conclusion In the above presentation, I have evaluated four cryptographic keycards for use with various OpenPGP operations. What the results show is that the only efficient way of storing a 4096-bit encryption key on a keycard would be to use the YubiKey 4. Unfortunately, I do not feel we should put our trust in such closed designs so I would argue you should either stick with 2048-bit encryption subkeys or keep the keys on disk. Considering that losing such a key would be catastrophic, this might be a good approach anyway. You should also consider switching to ECC encryption: even though it may not be supported everywhere, GnuPG supports having multiple encryption subkeys on a keyring: if one algorithm is unsupported (e.g. GnuPG 1.4 doesn't support ECC), it will fall back to a supported algorithm (e.g. RSA). Do not forget your previously encrypted material doesn't magically re-encrypt itself using your new encryption subkey, however. For authentication and signing keys, speed is not such an issue, so I would warmly recommend either the Nitrokey Pro or Start, or the FST-01, depending on whether you want to start experimenting with ECC algorithms. Availability also seems to be an issue for the FST-01. While you can generally get the device when you meet Niibe in person for a few bucks (I bought mine for around \$30 Canadian), the Seeed online shop says the device is out of stock at the time of this writing, even though Jonathan McDowell said that may be inaccurate in a debian-project discussion. Nevertheless, this issue may make the Nitrokey devices more attractive. When deciding on using the Pro or Start, Suhr offered the following advice:
In practice smart card security has been proven to work well (at least if you use a decent smart card). Therefore the Nitrokey Pro should be used for high security cases. If you don't trust the smart card or if Nitrokey Start is just sufficient for you, you can choose that one. This is why we offer both models.
So far, I have created a signing subkey and moved that and my authentication key to the YubiKey NEO, because it's a device I physically trust to keep itself together in my pockets and I was already using it. It has served me well so far, especially with its extra features like U2F and HOTP support, which I use frequently. Those features are also available on the Nitrokey Pro, so that may be an alternative if I lose the YubiKey. I will probably move my main certification key to the FST-01 and a LUKS-encrypted USB disk, to keep that certification key offline but backed up on two different devices. As for the encryption key, I'll wait for keycard performance to improve, or simply switch my whole keyring to ECC and use the FST-01 or Nitrokey Start for that purpose.
[The author would like to thank Nitrokey for providing hardware for testing.] This article first appeared in the Linux Weekly News.

15 October 2017

Norbert Preining: TeX Live Manager: JSON output

With the development of TLCockpit continuing, I found the need for and easy exchange format between the TeX Live Manager tlmgr and frontend programs like TLCockpit. Thus, I have implemented JSON output for the tlmgr info command. While the format is not 100% stable I might change some thing I consider it pretty settled. The output of tlmgr info --data json is a JSON array with JSON objects for each package requested (default is to list all). 
[ TLPackageObj, TLPackageObj, ... ]
The structure of the JSON object TLPackageObj reflects the internal Perl hash. Guaranteed to be present keys are name (String) and avilable (Boolean). In case the package is available, there are the following further keys sorted by their type: A rather long example showing the output for the package latex, formatted with json_pp and having the list of files and the long description shortened: 
[
    
      "installed" : true,
      "doccontainerchecksum" : "5bdfea6b85c431a0af2abc8f8df160b297ad73f6a324ca88df990f01f24611c9ae80d2f6d12c7b3767308fbe3de3fca3d11664b923ea4080fb13fd056a1d0c3d",
      "docfiles" : [
         "texmf-dist/doc/latex/base/README.txt",
         ....
         "texmf-dist/doc/latex/base/webcomp.pdf"
      ],
      "containersize" : 163892,
      "depends" : [
         "luatex",
         "pdftex",
         "latexconfig",
         "latex-fonts"
      ],
      "runsize" : 414,
      "relocated" : false,
      "doccontainersize" : 12812184,
      "srcsize" : 752,
      "revision" : 43813,
      "srcfiles" : [
         "texmf-dist/source/latex/base/alltt.dtx",
         ....
         "texmf-dist/source/latex/base/utf8ienc.dtx"
      ],
      "category" : "Package",
      "cataloguedata" :  
         "version" : "2017/01/01 PL1",
         "topics" : "format",
         "license" : "lppl1.3",
         "date" : "2017-01-25 23:33:57 +0100"
       ,
      "srccontainerchecksum" : "1d145b567cf48d6ee71582a1f329fe5cf002d6259269a71d2e4a69e6e6bd65abeb92461d31d7137f3803503534282bc0c5546e5d2d1aa2604e896e607c53b041",
      "postactions" : [],
      "binsize" :  ,
      "longdesc" : "LaTeX is a widely-used macro package for TeX, [...]",
      "srccontainersize" : 516036,
      "containerchecksum" : "af0ac85f89b7620eb7699c8bca6348f8913352c473af1056b7a90f28567d3f3e21d60be1f44e056107766b1dce8d87d367e7f8a82f777d565a2d4597feb24558",
      "executes" : [],
      "binfiles" :  ,
      "name" : "latex",
      "catalogue" : null,
      "docsize" : 3799,
      "available" : true,
      "runfiles" : [
         "texmf-dist/makeindex/latex/gglo.ist",
         ...
         "texmf-dist/tex/latex/base/x2enc.dfu"
      ],
      "shortdesc" : "A TeX macro package that defines LaTeX"
    
]
What is currently not available via tlmgr info and thus also not via the JSON output is access to virtual TeX Live databases with several member databases (multiple repositories). I am thinking about how to incorporate this information. These changes are currently available in the tlcritical repository, but will enter proper TeX Live repositories soon. Using this JSON output I will rewrite the current TLCockpit tlmgr interface to display more complete information.

14 October 2017

Norbert Preining: ScalaFX: ListView with CellFactory

I had a bit hard time to get ScalaFX to display a list of items in a scrollable space, and each item can be clicked. I use this in TLCockpit to display the list of documentation files in a TeX Live package, and open it directly from the application. Unfortunately there is not a huge amount of examples using ScalaFX out there in the web, so it took me a bit. My first try was using a VBox with various Labels in there, but this is not scrollable. In other areas I have used TreeTableView, so in this case using ListView should be fine. What I finally came up is the following code: 
import scalafx.application.JFXApp
import scalafx.application.JFXApp.PrimaryStage
import scalafx.collections.ObservableBuffer
import scalafx.geometry.Orientation
import scalafx.scene.control. ListCell, ListView 
import scalafx.scene.input.MouseEvent
import scalafx.scene. Cursor, Scene 
import scalafx.scene.paint.Color
import scalafx.Includes._
object ApplicationMain extends JFXApp  
  val SomeStrings: Seq[String] = Seq("Hello", "World", "Enjoy")
  stage = new PrimaryStage  
    title = "ListViewExample"
    scene = new Scene  
      root =  
        new ListView[String]  
          orientation = Orientation.Vertical
          cellFactory =  
            p =>  
              val cell = new ListCell[String]
              cell.textFill = Color.Blue
              cell.cursor = Cursor.Hand
              cell.item.onChange   (_, _, str) => cell.text = str  
              cell.onMouseClicked =   me: MouseEvent => println("Do something with " + cell.text.value)  
              cell
             
           
          items = ObservableBuffer(SomeStrings)
Some comments to the code, at least as far I understand it: Once managed, it doesn t look so complicated, but took me some time.

13 October 2017

Alex Muntada: My Free Software Activities in Jul-Sep 2017

If you read Planet Debian often, you ve probably noticed a trend of Free Software activity reports at the beginning of the month. First, those reports seemed a bit unamusing and lengthy, but since I take the time to read them I ve learnt a lot of things, and now I m amazed at the amount of work that people are doing for Free Software. Indeed, I knew already that many people are doing lots of work. But reading those reports gives you an actual view of how much it is. Then, I decided that I should do the same and write some kind of report since I became a Debian Developer in July. I think it s a nice way to share your work with others and maybe inspire them as it happened to me. So I asked some of the people that have been inspiring me how do they do it. I mean, I was curious to know how they keep track of the work they do and how long it takes to write their reports. It seems that it takes quite some time, it s mostly manual work and usually starts by the end of the month, reviewing their contributions in mailing lists, bug trackers, e-mail folders, etc. Here I am now, writing my first report about my Free Software activities since July and until September 2017. I hope you like it: Happy hacking!

Shirish Agarwal: I need to speak up now X Economics

Dear all, This would be a longish blog post (as most of mine are) compiled over days but as there is so short a time and so much to share. I had previously thought to share beautiful photographs of Ganesh mandals taking out the procession at time of immersion of the idol or the last day of Durga Puja recent events around do not make my mood to share photos at this point in time. I may share some of them in a future blog post or two . Before going further, I would like to offer my sympathies and condolences to people hurt and dislocated in Hurricane Irma , the 2017 Central Mexico Earthquake and lastly the most recent Las Vegas shooting as well as Hurricane Maria in Puerto Rico . I am somewhat nonplussed as to why Americans always want to name, especially hurricanes which destroy people s lives and livelihood built over generations and why most of the hurricanes are named after women. A look at weather.com site unveiled the answer to the mystery. Ironically (or not) I saw some of the best science coverage about Earthquakes or anything scientific reporting and analysis after a long time in mainstream newspapers in India. On another note, I don t understand or even expect to understand why the gunman did what he did 2 days back. Country music AFAIK is one of the most chilled-out kind of music, in some ways very similar to classical Indian singing although they are worlds apart in style of singing, renditions, artists, the way they emote etc. I seriously wish that the gunman had not been shot but caught and reasons were sought about what he did, he did. While this is certainly armchair thinking as was not at the scene of crime, but if a Mumbai Police constable could do it around a decade ago armed only with a lathi could do it, why couldn t the American cops who probably are trained in innumerable ways to subdue people without killing them, did. While investigations are on, I suspect if he were caught just like Ajmal Kasab was caught then lot of revelations might have come up. From what is known, the gentleman was upwardly mobile i.e. he was white, rich and apparently had no reason to have beef with anybody especially a crowd swaying to some nice music, all of which makes absolutely no sense. Indian Economy Slowdown Anyways, back to one of the main reasons of writing this blog post. Few days back, an ex-finance Minister of India Yashwant Sinha wrote what was felt by probably millions of Indians, an Indian Express article called I need to speak up now While there have been many, many arguments made since then by various people. A simple search of I need to speak up would lead to lead to many a result besides the one I have shared above. The only exception I have with the article is the line Forty leading companies of the country are already facing bankruptcy proceedings. Many more are likely to follow suit. I would not bore you but you ask any entrepreneur trying to set up shop in India i.e. ones who actually go through the processes of getting all the licenses for setting up even a small businesses as to the numerous hurdles they have to overcome and laid-back corrupt bureaucracy which they have to overcome. I could have interviewed some of my friends who had the conviction and the courage to set up shop and spent more than half a decade getting all the necessary licenses and approval to set up but it probably would be too specific for one industry or the other and would lead to the same result. Co-incidentally, a new restaurant, leaf opened in my vicinity few weeks before. From the looks it looked like a high-brow, high-priced restaurant hence like many others I did not venture in. After a few days, they introduced south-Indian delicacies like Masala Dosa, Uttapam at prices similar to other restaurants around. So I ventured in and bought some south Indian food to consume between mum and me. Few days later, I became friends with the owner/franchisee and I suggested (in a friendly tone) that why he doesn t make it like a CCD play where many people including yours truly use the service to share, strategize and meet with clients. The CCD joints usually serve coffee and snacks (which are over-priced but still run out pretty fast) but people come as they have chilled-out atmosphere and Wi-Fi access which people need for their smartphones, although the Wi-Fi part may soon become redundant With Reliance Jio making a big play. I also shared why he doesn t add more variety and time (the south Indian items are time-limited) as I see/saw many empty chairs there. Anyways, the shop-owner/franchisee shared his gross costs including salary, stocking, electricity, rent and it doesn t pan out to be serving Rs.80/- dish (roughly a 1US dollar and 25 cents) then serving INR Rs. 400/- a dish (around 6 $USD). One round of INR 400/- + dishes make his costs for the day, around 12 tables were there. It s when they have two full rounds of dishes costing INR 400/- or more that he actually has profits and he is predicting loss for at least 6 months to a year before he makes a rebound. He needs steady customers rather than just walk-ins that will make his business work/click. Currently his family is bearing the costs. He didn t mention the taxes although I know apart from GST there are still some local body taxes that they will have to pay and comply with. There are a multitude of problems for shutting a shop legally as well as they have to again renavigate the bureaucracy for the same. I have seen more than a few retailers downing their shutters for 6-8 months and then either sell it to new management, let go of the lease or simply sell the property to a competitor. The Insolvency and Bankruptcy Code is probably the first proper exit policy for large companies. So the 40 odd companies that Mr. Sinha were talking about were probably sick for a long time. In India, there is also an additional shame of being a failed entrepreneur unlike in the west where Entrepreneurs start on their next venture. As seen from Retailing In India only 3.3% of the population or at the most 4% of the population is directly or indirectly linked with the retail trade. Most of the economy still derives its wealth from the agrarian sector which is still reeling under the pressure from demonetization which happened last year. Al jazeera surprisingly portrayed a truer picture of the effects demonetization had on common citizen than many Indian newspapers did at the time. Because of the South African Debconf, I had to resort to debit cards and hence was able to escape standing in long lines in which many an old and women perished. It is only yesterday that the Government has acknowledged which many prominent Indians have been saying for months now, that we are in a slowdown . Be aware of the terms being used for effect by the Prime Minister. There are two articles which outlines the troubles India is in atm. The only bright spot has been e-commerce which so far has eluded GST although the Govt. has claimed regulations to put it in check. Indian Education System Interestingly, Ravish Kumar has started a series on NDTV where he is showcasing how Indian education sector, especially public colleges have been left to teachers on contract basis, see the first four episodes on NDTV channel starting with the first one I have shared as a hyperlink. I apologize as the series is in Hindi as the channel is meant for Indians and is mostly limited to Northern areas of the Country (mostly) although he has been honest that it is because they lack resources to tackle the amount of information flowing to them. Ravish started the series with sharing information about the U.S. where the things are similar with some teachers needing to sleep in cars because of high-cost of living to some needing to turn to sex-work . I was shocked when I read the guardian article, that is no way to treat our teachers.I went on to read How the American University was Killed following the breadcrumbs along the way. Reading that it seems Indians have been following the American system playbook from the 1980 s itself. The article talks about HMO as well and that seems to have followed here as well with my own experience of hospital fees and drugs which I had to entail a few weeks/month ago. Few years ago, when me and some of my friends had the teaching bug and we started teaching in a nearby municipal school, couple of teachers had shared that they were doing 2-3 jobs to make ends meet. I don t know about others in my group, at least I was cynical because I thought all the teachers were permanent and they make good money only to realize now that the person was probably speaking the truth. When you have to do three jobs to make ends meet from where do you bring the passion to teach young people and that too outside the syllabus ? Also, with this new knowledge in hindsight, I take back all my comments I made last year and the year before for the pathetic education being put up by the State. With teachers being paid pathetically/underpaid and almost 60% teachers being ad-hoc/adjunct teachers they have to find ways to have some sense of security. Most teachers are bachelors as they are poor and cannot offer any security (either male or female) and for women, after marriage it actually makes no sense for them to continue in this profession. I salute all the professors who are ad-hoc in nature and probably will never get a permanent position in their life. I think in some way, thanx to him, that the government has chosen to give 7th pay commisson salary to teachers. While the numbers may appear be large, there are a lot of questions as to how many people will actually get paid. There needs to be lot of vacancies which need to be filled quickly but don t see any solution in the next 2-3 years as well. The Government has taken a position to use/re-hire retired teachers rather than have new young teachers as an unwritten policy. In this Digital India context how are retired teachers supposed to understand and then pass on digital concepts is beyond me when at few teacher trainings I have seen they lack even the most basic knowledge that I learnt at least a decade or two ago, the difference is that vast. I just don t know what to say to that. My own experience with my own mother who had pretty good education in her time and probably would have made a fine business-woman if she knew that she will have a child that she would have to raise by herself alone (along with maternal grand-parents) is testimonial to the fact how hard it is for older people to grasp technology and here I m talking just using the interface as a consumer rather than a producer or someone in-between who has the idea of how companies and governments profit from whatever data is shared one way or the other. After watching the series/episodes and discussing the issue with my mother it was revealed that both her and my late maternal grandfather were on casual/ad-hoc basis till 20-25 years in their service in the defense sector. If Ravish were to do a series on the defense sector he probably would find the same thing there. To add to that, the defense sector is a vital component to a country s security. If 60% of the defense staff in all defense establishments have temporary staff how do you ensure the loyalty of the people working therein. That brings to my mind Ignorance is bliss . Software development and deployment There is another worry that all are skirting around, the present dispensation/government s mantra is minimum government-maximum governance with digital technologies having all solutions which is leading to massive unemployment. Also from most of the stories/incidents I read in the newspapers, mainstream media and elsewhere it seems most software deployments done in India are done without having any system of internal checks and balances. There is no lintian for software to be implemented. Contracts seem to be given to big companies and there is no mention of what prerequisites or conditions were laid down by the Government for software development and deployment and if any checks were done to ensure that the software being developed was in according to government specifications or not. Ideally this should all be in public domain so that questions can be asked and responsibility fixed if things go haywire, as currently they do not. Software issues As my health been not that great, I have been taking a bit more time and depth while filing bugs. #877638 is a good example. I suspect though that part of the problem might be that mate has moved to gtk3 while guake still has gtk-2 bindings. I also reported the issue upstream both in mate-panel as well as guake . I haven t received any response from either or/and upstreams . I also have been fiddling around with gdb to better understand the tool so I can exploit/use this tool in a better way. There are some commands within the gdb interface which seem to be interesting and hopefully I ll try how the commands perform over days, weeks to a month. I hope we see more action on the mate-panel/guake bug as well as move of guake to gtk+3 but that what seemingly seemed like wait for eternity seems to have done by somebody in last couple of days. As shared in the ticket there are lots of things still to do but it seems the heavy lifting has been done but seems merging will be tricky as two developers have been trying to update to gtk+3 although aichingm seems to have a leg up with his 3! branch. Another interesting thing I saw is the below picture. Firefox is out of date on wordpress.com The firefox version I was using to test the site/wordpress-wp-admin was Mozilla Firefox 52.4.0 which AFAIK is a pretty recentish one and people using Debian stretch would probably be using the same version (firefox stable/LTS) rather than the more recent versions. I went to the link it linked to and it gave no indication as to why it thought my browser is out-of-date and what functionality was/is missing. I have found that wordpress support has declined quite a bit and people don t seem to use the forums as much as they used to before. I also filed a few bugs for qalculate. #877716 where a supposedly transitional package removes the actual application, #877717 as the software has moved its repo. to github.com as well as tickets and other things in process and lastly #877733. I had been searching for a calculator which can do currency calculations on the fly (say for e.g. doing personal budgeting for Taiwan debconf) without needing to manually enter the conversion rates and losing something in the middle. While the current version has support for some limited currencies, the new versions promise more as other people probably have more diverse needs for currency conversions (people who do long or short on oil, stocks overseas is just one example, I am sure there are many others) than simplistic mine.
Filed under: Miscellenous Tagged: #American Education System, #bug-filing, #Climate change, #Dignity, #e-commerce, #gtk+3, #gtk2, #Indian Economy 'Slowdown', #Indian Education System, #Insolvency and Bankruptcy Code, #Las Vegas shooting, #Modern Retail in India, #planet-debian, #qalculate, Ad-hoc and Adjunct Professors, wordpress.com

12 October 2017

Joachim Breitner: Isabelle functions: Always total, sometimes undefined

Often, when I mention how things work in the interactive theorem prover [Isabelle/HOL] (in the following just Isabelle 1) to people with a strong background in functional programming (whether that means Haskell or Coq or something else), I cause confusion, especially around the issue of what is a function, are function total and what is the business with undefined. In this blog post, I want to explain some these issues, aimed at functional programmers or type theoreticians. Note that this is not meant to be a tutorial; I will not explain how to do these things, and will focus on what they mean.

HOL is a logic of total functions If I have a Isabelle function f :: a b between two types a and b (the function arrow in Isabelle is , not ), then by definition of what it means to be a function in HOL whenever I have a value x :: a, then the expression f x (i.e. f applied to x) is a value of type b. Therefore, and without exception, every Isabelle function is total. In particular, it cannot be that f x does not exist for some x :: a. This is a first difference from Haskell, which does have partial functions like 
spin :: Maybe Integer -> Bool
spin (Just n) = spin (Just (n+1))
Here, neither the expression spin Nothing nor the expression spin (Just 42) produce a value of type Bool: The former raises an exception ( incomplete pattern match ), the latter does not terminate. Confusingly, though, both expressions have type Bool. Because every function is total, this confusion cannot arise in Isabelle: If an expression e has type t, then it is a value of type t. This trait is shared with other total systems, including Coq. Did you notice the emphasis I put on the word is here, and how I deliberately did not write evaluates to or returns ? This is because of another big source for confusion:

Isabelle functions do not compute We (i.e., functional programmers) stole the word function from mathematics and repurposed it2. But the word function , in the context of Isabelle, refers to the mathematical concept of a function, and it helps to keep that in mind. What is the difference?
  • A function a b in functional programming is an algorithm that, given a value of type a, calculates (returns, evaluates to) a value of type b.
  • A function a b in math (or Isabelle) associates with each value of type a a value of type b.
For example, the following is a perfectly valid function definition in math (and HOL), but could not be a function in the programming sense: 
definition foo :: "(nat   real)   real" where
  "foo seq = (if convergent seq then lim seq else 0)"
This assigns a real number to every sequence, but it does not compute it in any useful sense. From this it follows that

Isabelle functions are specified, not defined Consider this function definition: 
fun plus :: "nat   nat   nat"  where
   "plus 0       m = m"
   "plus (Suc n) m = Suc (plus n m)"
To a functional programmer, this reads
plus is a function that analyses its first argument. If that is 0, then it returns the second argument. Otherwise, it calls itself with the predecessor of the first argument and increases the result by one.
which is clearly a description of a computation. But to Isabelle, the above reads
plus is a binary function on natural numbers, and it satisfies the following two equations:
And in fact, it is not so much Isabelle that reads it this way, but rather the fun command, which is external to the Isabelle logic. The fun command analyses the given equations, constructs a non-recursive definition of plus under the hood, passes that to Isabelle and then proves that the given equations hold for plus. One interesting consequence of this is that different specifications can lead to the same functions. In fact, if we would define plus' by recursing on the second argument, we d obtain the the same function (i.e. plus = plus' is a theorem, and there would be no way of telling the two apart).

Termination is a property of specifications, not functions Because a function does not evaluate, it does not make sense to ask if it terminates. The question of termination arises before the function is defined: The fun command can only construct plus in a way that the equations hold if it passes a termination check very much like Fixpoint in Coq. But while the termination check of Fixpoint in Coq is a deep part of the basic logic, in Isabelle it is simply something that this particular command requires for its internal machinery to go through. At no point does a termination proof of the function exist as a theorem inside the logic. And other commands may have other means of defining a function that do not even require such a termination argument! For example, a function specification that is tail-recursive can be turned in to a function, even without a termination proof: The following definition describes a higher-order function that iterates its first argument f on the second argument x until it finds a fixpoint. It is completely polymorphic (the single quote in 'a indicates that this is a type variable): 
partial_function (tailrec)
  fixpoint :: "('a   'a)   'a   'a"
where
  "fixpoint f x = (if f x = x then x else fixpoint f (f x))"
We can work with this definition just fine. For example, if we instantiate f with ( x. x-1), we can prove that it will always return 0: 
lemma "fixpoint (  n . n - 1) (n::nat) = 0"
  by (induction n) (auto simp add: fixpoint.simps)
Similarly, if we have a function that works within the option monad (i.e. Maybe in Haskell), its specification can always be turned into a function without an explicit termination proof here one that calculates the Collatz sequence: 
partial_function (option) collatz :: "nat   nat list option"
 where "collatz n =
        (if n = 1 then Some [n]
         else if even n
           then do   ns <- collatz (n div 2);    Some (n # ns)  
           else do   ns <- collatz (3 * n + 1);  Some (n # ns) )"
Note that lists in Isabelle are finite (like in Coq, unlike in Haskell), so this function returns a list only if the collatz sequence eventually reaches 1. I expect these definitions to make a Coq user very uneasy. How can fixpoint be a total function? What is fixpoint ( n. n+1)? What if we run collatz n for a n where the Collatz sequence does not reach 1?3 We will come back to that question after a little detour

HOL is a logic of non-empty types Another big difference between Isabelle and Coq is that in Isabelle, every type is inhabited. Just like the totality of functions, this is a very fundamental fact about what HOL defines to be a type. Isabelle gets away with that design because in Isabelle, we do not use types for propositions (like we do in Coq), so we do not need empty types to denote false propositions. This design has an important consequence: It allows the existence of a polymorphic expression that inhabits any type, namely 
undefined :: 'a
The naming of this term alone has caused a great deal of confusion for Isabelle beginners, or in communication with users of different systems, so I implore you to not read too much into the name. In fact, you will have a better time if you think of it as arbitrary or, even better, unknown. Since undefined can be instantiated at any type, we can instantiate it for example at bool, and we can observe an important fact: undefined is not an extra value besides the usual ones . It is simply some value of that type, which is demonstrated in the following lemma: 
lemma "undefined = True   undefined = False" by auto
In fact, if the type has only one value (such as the unit type), then we know the value of undefined for sure: 
lemma "undefined = ()" by auto
It is very handy to be able to produce an expression of any type, as we will see as follows

Partial functions are just underspecified functions For example, it allows us to translate incomplete function specifications. Consider this definition, Isabelle s equivalent of Haskell s partial fromJust function: 
fun fromSome :: "'a option   'a" where
  "fromSome (Some x) = x"
This definition is accepted by fun (albeit with a warning), and the generated function fromSome behaves exactly as specified: when applied to Some x, it is x. The term fromSome None is also a value of type 'a, we just do not know which one it is, as the specification does not address that. So fromSome None behaves just like undefined above, i.e. we can prove 
lemma "fromSome None = False   fromSome None = True" by auto
Here is a small exercise for you: Can you come up with an explanation for the following lemma: 
fun constOrId :: "bool   bool" where
  "constOrId True = True"
lemma "constOrId = ( _.True)   constOrId = ( x. x)"
  by (metis (full_types) constOrId.simps)
Overall, this behavior makes sense if we remember that function definitions in Isabelle are not really definitions, but rather specifications. And a partial function definition is simply a underspecification. The resulting function is simply any function hat fulfills the specification, and the two lemmas above underline that observation.

Nonterminating functions are also just underspecified Let us return to the puzzle posed by fixpoint above. Clearly, the function seen as a functional program is not total: When passed the argument ( n. n + 1) or ( b. b) it will loop forever trying to find a fixed point. But Isabelle functions are not functional programs, and the definitions are just specifications. What does the specification say about the case when f has no fixed-point? It states that the equation fixpoint f x = fixpoint f (f x) holds. And this equation has a solution, for example fixpoint f _ = undefined. Or more concretely: The specification of the fixpoint function states that fixpoint ( b. b) True = fixpoint ( b. b) False has to hold, but it does not specify which particular value (True or False) it should denote any is fine.

Not all function specifications are ok At this point you might wonder: Can I just specify any equations for a function f and get a function out of that? But rest assured: That is not the case. For example, no Isabelle command allows you define a function bogus :: () nat with the equation bogus () = Suc (bogus ()), because this equation does not have a solution. We can actually prove that such a function cannot exist: 
lemma no_bogus: "  bogus. bogus () = Suc (bogus ())" by simp
(Of course, not_bogus () = not_bogus () is just fine )

You cannot reason about partiality in Isabelle We have seen that there are many ways to define functions that one might consider partial . Given a function, can we prove that it is not partial in that sense? Unfortunately, but unavoidably, no: Since undefined is not a separate, recognizable value, but rather simply an unknown one, there is no way of stating that A function result is not specified . Here is an example that demonstrates this: Two partial functions (one with not all cases specified, the other one with a self-referential specification) are indistinguishable from the total variant: 
fun partial1 :: "bool   unit" where
  "partial1 True = ()"
partial_function (tailrec) partial2 :: "bool   unit" where
  "partial2 b = partial2 b"
fun total :: "bool   unit" where
  "total True = ()"
  "total False = ()"
lemma "partial1 = total   partial2 = total" by auto
If you really do want to reason about partiality of functional programs in Isabelle, you should consider implementing them not as plain HOL functions, but rather use HOLCF, where you can give equational specifications of functional programs and obtain continuous functions between domains. In that setting, () and partial2 = total. We have done that to verify some of HLint s equations.

You can still compute with Isabelle functions I hope by this point, I have not scared away anyone who wants to use Isabelle for functional programming, and in fact, you can use it for that. If the equations that you pass to fun are a reasonable definition for a function (in the programming sense), then these equations, used as rewriting rules, will allow you to compute that function quite like you would in Coq or Haskell. Moreover, Isabelle supports code extraction: You can take the equations of your Isabelle functions and have them expored into Ocaml, Haskell, Scala or Standard ML. See Concon for a conference management system with confidentially verified in Isabelle. While these usually are the equations you defined the function with, they don't have to: You can declare other proved equations to be used for code extraction, e.g. to refine your elegant definitions to performant ones. Like with code extraction from Coq to, say, Haskell, the adequacy of the translations rests on a moral reasoning foundation. Unlike extraction from Coq, where you have an (unformalized) guarantee that the resulting Haskell code is terminating, you do not get that guarantee from Isabelle. Conversely, this allows you do reason about and extract non-terminating programs, like fixpoint, which is not possible in Coq. There is currently ongoing work about verified code generation, where the code equations are reflected into a deep embedding of HOL in Isabelle that would allow explicit termination proofs.

Conclusion We have seen how in Isabelle, every function is total. Function declarations have equations, but these do not define the function in an computational sense, but rather specify them. Because in HOL, there are no empty types, many specifications that appear partial (incomplete patterns, non-terminating recursion) have solutions in the space of total functions. Partiality in the specification is no longer visible in the final product.

PS: Axiom undefined in Coq This section is speculative, and an invitation for discussion. Coq already distinguishes between types used in programs (Set) and types used in proofs Prop. Could Coq ensure that every t : Set is non-empty? I imagine this would require additional checks in the Inductive command, similar to the checks that the Isabelle command datatype has to perform4, and it would disallow Empty_set. If so, then it would be sound to add the following axiom 
Axiom undefined : forall (a : Set), a.
wouldn't it? This axiom does not have any computational meaning, but that seems to be ok for optional Coq axioms, like classical reasoning or function extensionality. With this in place, how much of what I describe above about function definitions in Isabelle could now be done soundly in Coq. Certainly pattern matches would not have to be complete and could sport an implicit case _ undefined. Would it help with non-obviously terminating functions? Would it allow a Coq command Tailrecursive that accepts any tailrecursive function without a termination check?
  1. Isabelle is a metalogical framework, and other logics, e.g. Isabelle/ZF, behave differently. For the purpose of this blog post, I always mean Isabelle/HOL.
  2. Isabelle is a metalogical framework, and other logics, e.g. Isabelle/ZF, behave differently. For the purpose of this blog post, I always mean Isabelle/HOL.
  3. Let me know if you find such an n. Besides n = 0.
  4. Like fun, the constructions by datatype are not part of the logic, but create a type definition from more primitive notions that is isomorphic to the specified data type.

Next.

Previous.