Code Monkey home page Code Monkey logo

jwx's Introduction

Build Status

JWX is a library for handling JSON data and more. It is implemented in the SPARK programming language and has been proven to contain no runtime errors. As a result, JWX is particularly suited for processing untrusted information.

In version 0.5.0 of JWX, parsing of Base64 (RFC 4648) data, JSON (RFC 8259) documents, JSON Web Keys (JWK, RFC 7517) and limited support for JSON Web Signatures (JWS, RFC 7515) and JSON Web Tokens (JWT, RFC 7519) is implemented. In the future, JSON Web Encryption (JWE, RFC 7516) and potentially JSON Schema is anticipated.

JWX is available under the AGPLv3 license. For commercial licensing and support mail to [email protected].

Examples

API documentation is available here.

Parsing Base64 data

with Ada.Text_IO; use Ada.Text_IO;
with JWX.Util;
with JWX.Base64;

procedure B64 is
   use JWX;
   Len    : Natural;
   Bytes  : Byte_Array (1..50);
   Result : String (1..50);
begin
   Base64.Decode (Encoded => "Zm9vYmFy", Length => Len, Result => Bytes);
   if Len > 0 then
      Util.To_String (Bytes, Result);
      Put_Line (Result (1 .. Len)); -- "foobar"
   end if;
end B64;

Parsing JSON document

with Ada.Text_IO; use Ada.Text_IO;
with JWX.JSON;

procedure JSON is
   Data : String := " { ""precision"": ""zip"", ""Latitude"":  37.7668, ""Longitude"": -122.3959, ""Address"": """", ""City"": ""SAN FRANCISCO"", ""State"": ""CA"", ""Zip"": ""94107"", ""Country"": ""US"" }";
   package J is new JWX.JSON (Data);
   use J;
   Result : Index_Type;
   Match : Match_Type;
begin
   Parse (Match);
   if Match = Match_OK and then Get_Kind = Kind_Object
   then
      Result := Query_Object ("City");
      Put_Line ("City: " & Get_String (Result)); -- "SAN FRANCISCO"

      Result := Query_Object ("Latitude");
      Put_Line ("Lat.: " & Get_Real (Result)'Img); -- 37.7668
   end if;
end JSON;

Validating a JSON web token

with Ada.Text_IO; use Ada.Text_IO;
with JWX.JWT; use JWX.JWT;
with JWX_Test_Utils;

procedure JWT is
   Tmp  : String := JWX_Test_Utils.Read_File ("tests/data/JWT_test_data.dat");
   Key  : String := JWX_Test_Utils.Read_File ("tests/data/HTTP_auth_key.json");
   Data : String := Tmp (Tmp'First .. Tmp'Last - 1);
   package J renames Standard.JWX.JWT;
   Result : J.Result_Type;
begin
   Result := J.Validate_Compact (Data     => Data,
                                 Key_Data => Key,
                                 Audience => "4cCy0QeXkvjtHejID0lKzVioMfTmuXaM",
                                 Issuer   => "https://cmpnlt-demo.eu.auth0.com/",
                                 Now      => 1528404620);
   if Result = Result_OK then
      Put_Line ("Token is valid");
   end if;
end JWT;

Limitations

The following known limitations exist in JWX:

  • While absence of runtime errors has been proven, no formal analysis for the stack usage exists
  • Generation of Base64, JSON, JWS, JWT etc. is not supported (only validation)
  • Unicode is not supported
  • JWS and JWT only support HMAC-SHA256 (no other HMAC modes, RSA or ECDSA)
  • JWS JSON serialization is not supported (only JWS compact serialization)
  • Only the registered claims iss, exp and aud are supported
  • No scopes or custom claims are supported

Building

Check out JWX and build it:

$ git clone --recursive https://github.com/Componolit/jwx.git
$ cd jwx
$ make

To build the test cases, AUnit must be in your project path. To build an run the tests do:

$ make test

License

AGPLv3, see LICENSE file for details.

Contact

[email protected] or through the issue tracker at https://github.com/Componolit/jwx

jwx's People

Contributors

senier avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar

jwx's Issues

global item must denote object, state or current instance of concurrent type

When trying to build the amatrix library example I get the following error:

$ gprbuild -P amatrix_examples.gpr                                                                                                                                                                       
gnatgcc -c example_client.adb
example_client.adb:16:07: instantiation error at jwx-json.adb:754
example_client.adb:16:07: instantiation error at amatrix-client.adb:28
example_client.adb:16:07: global item must denote object, state or current instance of concurrent type
gprbuild: *** compilation phase failed

It seems to happen when I instantiate the JWX.JSON package. The json example from jwx itself works without problems. The same error happens when compiling it on Genode. I also don't really understand the lobal item must denote object, state or current instance of concurrent type message.

Update to Community 2020

In Community 2019 the current version triggers a bug box in gnatprove that does not happen in Pro 20.1:

Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
+===========================GNAT BUG DETECTED==============================+
| Community 2019 (20190517) (spark) GCC error:                             |
| could not add file /app/obj/gnatprove/jwx-jwt.mlw to the session:        |
|     File "jwx-json.adb", line 496, characters 0-0:
                                                                  this expression raises unlisted exception Temp___exception_688|
| No source file position information available                            |
| Please submit a bug report by email to [email protected].               |
| GAP members can alternatively use GNAT Tracker:                          |
| http://www.adacore.com/ section 'send a report'.                         |
| See gnatinfo.txt for full info on procedure for submitting bugs.         |
| Use a subject line meaningful to you and us to track the bug.            |
| Include the entire contents of this bug box in the report.               |
| Include the exact command that you entered.                              |
| Also include sources listed below.                                       |
| Use plain ASCII or MIME attachment(s).                                   |
+==========================================================================+

Please include these source files with error report
Note that list may not be accurate in some cases,
so please double check that the problem can still
be reproduced with the set of files listed.
Consider also -gnatd.n switch (see debug.adb).

/app/src/jwx-jwt.adb
/app/src/jwx-jwt.ads
/app/src/jwx.ads
/app/src/jwx-jws.ads
/app/src/jwx-json.ads
/app/src/jwx-base64.ads
/app/src/jwx-util.ads
/app/src/jwx-json.adb

compilation abandoned
gnatprove: error during flow analysis and proof
make: *** [Makefile:8: all] Error 1

Update CI

Move CI to GitHub actions and update to recent toolchain.

Fix flow errors

When proving master (and 0.5.0) a number of flow errors are revealed with current SPARK versions:

Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
src/proof_json.adb:25:07: high: constant with variable input "Context_Size" must be listed in the Global aspect of "Do_Parse" (SPARK RM 6.1.4(14))
src/jwx-json.adb:823:30: medium: overflow check might fail, in instantiation at proof_json.adb:19
src/jwx-json.adb:823:30: medium: range check might fail, in instantiation at proof_json.adb:19
src/jwx-json.adb:827:23: medium: overflow check might fail, in instantiation at proof_json.adb:19 (e.g. when Tmp = 9223372036854775809/131072)
src/jwx-json.adb:827:23: medium: range check might fail, in instantiation at proof_json.adb:19 (e.g. when Tmp = 9223372036854775809/131072)
src/jwx-libsparkcrypto.adb:31:14: warning: unused assignment
src/jwx-libsparkcrypto.adb:61:14: warning: unused assignment
src/jwx-jws.adb:31:12: high: constant with variable input "Data" must be listed in the Global aspect of "Validate_Compact" (SPARK RM 6.1.4(14))
src/jwx-jws.adb:54:11: high: constant with variable input "Key" must be listed in the Global aspect of "Validate_Compact" (SPARK RM 6.1.4(14))
src/jwx-jws.adb:54:11: high: constant with variable input "Payload" must be listed in the Global aspect of "Validate_Compact" (SPARK RM 6.1.4(14))
src/jwx-jws.adb:54:11: high: constant with variable input "Auth" must be listed in the Global aspect of "Validate_Compact" (SPARK RM 6.1.4(14))
src/jwx-crypto.adb:77:11: high: constant with variable input "Data" must be listed in the Global aspect of "Valid_HMAC_SHA256" (SPARK RM 6.1.4(14)), in instantiation at jwx-jws.adb:44
src/jwx-jose.adb:72:13: high: constant with variable input "Context_Size" must be listed in the Global aspect of "Decode" (SPARK RM 6.1.4(14)), in instantiation at jwx-jws.adb:43
src/jwx-json.adb:823:30: medium: overflow check might fail, in instantiation at jwx-jose.adb:66, in instantiation at jwx-jws.adb:43
src/jwx-json.adb:823:30: medium: range check might fail, in instantiation at jwx-jose.adb:66, in instantiation at jwx-jws.adb:43
src/jwx-json.adb:823:30: medium: overflow check might fail, in instantiation at jwx-jwk.adb:24, in instantiation at jwx-crypto.adb:39, in instantiation at jwx-jws.adb:44
src/jwx-json.adb:823:30: medium: range check might fail, in instantiation at jwx-jwk.adb:24, in instantiation at jwx-crypto.adb:39, in instantiation at jwx-jws.adb:44
src/jwx-json.adb:827:23: medium: overflow check might fail, in instantiation at jwx-jose.adb:66, in instantiation at jwx-jws.adb:43 (e.g. when Tmp = 9223372036854775809/131072)
src/jwx-json.adb:827:23: medium: range check might fail, in instantiation at jwx-jose.adb:66, in instantiation at jwx-jws.adb:43 (e.g. when Tmp = 9223372036854775809/131072)
src/jwx-json.adb:827:23: medium: overflow check might fail, in instantiation at jwx-jwk.adb:24, in instantiation at jwx-crypto.adb:39, in instantiation at jwx-jws.adb:44 (e.g. when Tmp = 9223372036854775809/131072)
src/jwx-json.adb:827:23: medium: range check might fail, in instantiation at jwx-jwk.adb:24, in instantiation at jwx-crypto.adb:39, in instantiation at jwx-jws.adb:44 (e.g. when Tmp = 9223372036854775809/131072)
src/jwx-jwk.adb:402:15: high: constant with variable input "Context_Size" must be listed in the Global aspect of "Parse_Keys" (SPARK RM 6.1.4(14)), in instantiation at jwx-crypto.adb:39, in instantiation at jwx-jws.adb:44
src/jwx-jwt.adb:82:16: high: constant with variable input "Context_Size" must be listed in the Global aspect of "Validate_Compact" (SPARK RM 6.1.4(14))
src/jwx-json.adb:823:30: medium: overflow check might fail, in instantiation at jwx-jwt.adb:76
src/jwx-json.adb:823:30: medium: range check might fail, in instantiation at jwx-jwt.adb:76
src/jwx-json.adb:827:23: medium: overflow check might fail, in instantiation at jwx-jwt.adb:76 (e.g. when Tmp = 9223372036854775809/131072)
src/jwx-json.adb:827:23: medium: range check might fail, in instantiation at jwx-jwt.adb:76 (e.g. when Tmp = 9223372036854775809/131072)
$ gnatprove --version
SPARK Pro 20.1 (20200107)
Why3 for gnatprove version 1.2.0+git
/opt/SPARK-Pro-20.1/libexec/spark/bin/alt-ergo: Alt-Ergo version 2.3.0+
/opt/SPARK-Pro-20.1/libexec/spark/bin/cvc4: This is CVC4 version 1.7.1-prerelease
/opt/SPARK-Pro-20.1/libexec/spark/bin/z3: Z3 version 4.8.4 - 64 bit

In addition, SPARK Community 2019 emits a bug box which is fixed in more recent versions and which likely will vanish in Community 2019 once the flow issues above are fixed:

Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
+===========================GNAT BUG DETECTED==============================+
| Community 2019 (20190517) (spark) GCC error:                             |
| could not add file obj/gnatprove/proof_json   |
|    .mlw to the session:
File "jwx-json.adb", line 496, characters 0-0:
this expression raises unlisted exception Temp___exception_627             |
| No source file position information available                            |
| Please submit a bug report by email to [email protected].               |
| GAP members can alternatively use GNAT Tracker:                          |
| http://www.adacore.com/ section 'send a report'.                         |
| See gnatinfo.txt for full info on procedure for submitting bugs.         |
| Use a subject line meaningful to you and us to track the bug.            |
| Include the entire contents of this bug box in the report.               |
| Include the exact command that you entered.                              |
| Also include sources listed below.                                       |
| Use plain ASCII or MIME attachment(s).                                   |
+==========================================================================+

Please include these source files with error report
Note that list may not be accurate in some cases,
so please double check that the problem can still
be reproduced with the set of files listed.
Consider also -gnatd.n switch (see debug.adb).

src/proof_json.adb
src/proof_json.ads
src/jwx.ads
src/jwx-json.ads
src/jwx-json.adb

src/proof_json.adb:25:07: high: constant with variable input "Context_Size" must be listed in the Global aspect of "Do_Parse" (SPARK RM 6.1.4(13))
compilation abandoned

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.