web analytics
Newspapers

 
Categories: Compiler

GCC 12.0.1 build on Mac OS-X 10.11 El Capitan, compatible SPARK2014

GNAT (FSF) ~ GCC 12.0.1 of 20220128 (only Ada, C, C++, built on Mac OS-X El Capitan, runs up to macOS 12 Monterey).
Compilers included: Ada, C, C++.
GNAT (FSF) Available on Simon’s GitHub

SPARK2014 built against it (provers CVC4, Z3, Alt-Ergo; CVC4 requires Sierra and upwards).
Needs GCC 12.0.1 installed.
SPARK2014 Available on Simon’s GitHub

Categories: Tech Library

ASN.1 implementation in SPARK, version 0.0.01

I'm making public my ASN.1 project which aims to be a verified implementation of ASN.1, which is used in security-certificates, which is hopefully the first step in a verified-TLS/-TLS -- the project also aims to be [directly] usable in DSA projects.

As of 0.0.01 the only portion implemented is a pure big-number package, and another currently shared-passive unit for usability.
I would certainly appropriate comments, criticism, and most especially contributions.

https://github.com/OneWingedShark/ASN.1/

Categories: Framework

Muen microkernel 0.7 released

The Muen Separation Kernel is the world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. It is developed in Switzerland by the Institute for Internet Technologies and Applications (ITA) at the University of Applied Sciences Rapperswil (HSR).

The following major features and improvements have been implemented :

  • Support for Genode VM subjects
  • Subject time mechanism
  • Hardware and platform policy abstractions
  • Linux virtual filesystem and network interface drivers

EEC GDPR compliant