ada-libraries
/
jwx
mirror of https://github.com/Componolit/jwx
1
0
Fork 0
Code Issues Releases Wiki Activity

Proof JWT handling

This commit is contained in:
Alexander Senier 2018-07-26 20:06:38 +02:00
parent 7fe9c05f2d
commit d761dd6a50
6 changed files with 124 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/jwx-json.adb
View File

@ -379,7 +379,8 @@ is
function Match_Set (Set : String) return Boolean
with
Post => (if Match_Set'Result then (for some E of Set => E = Data (Data'First + Offset)));
Global => (Input => (Data, Offset)),
Post => (if Match_Set'Result then (for some E of Set => E = Data (Data'First + Offset)));
function Match_Set (Set : String) return Boolean
is
@ -813,7 +814,8 @@ is
procedure Parse_String (Match : out Match_Type)
with
Global => (In_Out => (Context,
Global => (Input => (Data, CS),
In_Out => (Context,
Context_Index,
Offset));

9
src/jwx-json.ads
View File

@ -12,12 +12,12 @@
generic
Input_Data : String;
Context_Size : Natural := Input_Data'Length/3 + 2;
Context_Size : Natural := Input_Data'Length / 3 + 2;
package JWX.JSON
with
Abstract_State => State,
Initializes => (State, Data)
Initializes => (State, Data, CS, Null_Index, End_Index)
is
@ -40,7 +40,8 @@ is
Match_Invalid,
Match_Out_Of_Memory);
type Index_Type is new Natural range 1 .. Context_Size;
CS : constant Natural := Context_Size;
type Index_Type is new Natural range 1 .. CS;
Null_Index : constant Index_Type := Index_Type'First;
End_Index : constant Index_Type := Index_Type'Last;
@ -58,7 +59,7 @@ is
-- Return kind of current element of a context
function Get_Kind (Index : Index_Type := Null_Index) return Kind_Type
with
Global => (Input => State),
Global => (Input => (State)),
Post => Has_Kind (Index, Get_Kind'Result);
-- Return value of a boolean context element

135
src/jwx-jwt.adb
View File

@ -25,6 +25,12 @@ is
begin
Result := Result_Invalid;
if Data'Length >= Integer'Last - 2 or
Data'Length <= 0
then
return;
end if;
J.Validate_Compact (Validate_Result);
if Validate_Result /= J.Result_OK
then
@ -37,82 +43,99 @@ is
return;
end if;
pragma Assert (Data'Length < Integer'Last);
declare
Data : constant String := J.Payload;
use Base64;
Len : Natural;
Decoded : Byte_Array (1 .. 3 * ((Data'Length + 3) / 4));
JSON_Input : String (1 .. Data'Length);
Len : Natural;
Payload : constant String := J.Payload;
begin
Decode_Url (Data, Len, Decoded);
if Len = 0
if Payload'Length <= 0 or
Payload'Length >= Natural'Last / 9 or
Payload'Last >= Natural'Last - 4
then
Result := Result_Invalid_Base64;
return;
end if;
Util.To_String (Decoded, JSON_Input);
declare
Input : constant String := JSON_Input;
package Token is new JWX.JSON (Input);
use Token;
Match : Match_Type;
Value : Index_Type;
JSON_Input : String (1 .. Payload'Length + 2);
Decoded : Byte_Array (1 .. 3 * ((Payload'Length + 3) / 4));
use Base64;
begin
Parse (Match);
if Match /= Match_OK
Decode_Url (Payload, Len, Decoded);
if Len = 0
then
return;
end if;
if Get_Kind /= Kind_Object
then
Result := Result_Invalid_Object;
Result := Result_Invalid_Base64;
return;
end if;
-- Check issuer
Result := Result_Invalid_Issuer;
Value := Query_Object ("iss");
if Value = End_Index
then
return;
end if;
pragma Assert (JSON_Input'Length >= 3 * ((Payload'Length + 3) / 4));
Util.To_String (Decoded, JSON_Input);
if Get_String (Value) /= Issuer
then
return;
end if;
declare
Input : constant String := JSON_Input;
package Token is new JWX.JSON (Input);
use Token;
Match : Match_Type;
Value : Index_Type;
begin
Parse (Match);
if Match /= Match_OK
then
return;
end if;
if Get_Kind /= Kind_Object
then
Result := Result_Invalid_Object;
return;
end if;
-- Check audience
Result := Result_Invalid_Audience;
Value := Query_Object ("aud");
if Value = End_Index
then
return;
end if;
-- Check issuer
Result := Result_Invalid_Issuer;
Value := Query_Object ("iss");
if Value = End_Index
then
return;
end if;
if Get_String (Value) /= Audience
then
return;
end if;
if Get_Kind (Value) /= Kind_String or else
Get_String (Value) /= Issuer
then
return;
end if;
-- Check expiration
Result := Result_Expired;
Value := Query_Object ("exp");
if Value = End_Index
then
return;
end if;
-- Check audience
Result := Result_Invalid_Audience;
Value := Query_Object ("aud");
if Value = End_Index
then
return;
end if;
if Long_Integer (Get_Integer (Value)) < Now
then
return;
end if;
if Get_Kind (Value) /= Kind_String or else
Get_String (Value) /= Audience
then
return;
end if;
-- Check expiration
Result := Result_Expired;
Value := Query_Object ("exp");
if Value = End_Index
then
return;
end if;
if Get_Kind (Value) /= Kind_Integer or else
Long_Integer (Get_Integer (Value)) < Now
then
return;
end if;
end;
end;
Result := Result_OK;
return ;
return;
end;
end Validate_Compact;

44
src/jwx-stream_auth.adb
View File

@ -22,7 +22,7 @@ is
is
First : Natural := Buf'Last;
Last : Natural := Buf'First;
Auth : Auth_Result_Type := Auth_Noent;
Found : Boolean := False;
begin
-- At least space for 'id_token=' must be available
if Buf'Length < 10
@ -36,26 +36,44 @@ is
if Buf (I .. I + 8) = "id_token="
then
First := I + 9;
end if;
end loop;
-- Search end of ID token (next ampersand)
for I in First .. Buf'Last
loop
if Buf (I) = '&' or
Buf (I) = ' '
then
Last := I - 1;
Auth := Auth_Fail;
Found := True;
pragma Assert (First >= Buf'First);
exit;
end if;
end loop;
if Auth = Auth_Noent
if not Found or
not (First in Buf'Range)
then
return Auth_Noent;
end if;
-- Search end of ID token (next ampersand)
Found := False;
for I in First .. Buf'Last
loop
pragma Loop_Invariant (First >= Buf'First);
pragma Loop_Invariant (I <= Buf'Last);
if Buf (I) = '&' or
Buf (I) = ' '
then
Last := I - 1;
Found := True;
exit;
end if;
end loop;
if not Found or
not (Last in Buf'Range) or
not (First <= Last)
then
return Auth_Noent;
end if;
pragma Assert (First <= Last);
pragma Assert (First >= Buf'First);
pragma Assert (Last <= Buf'Last);
declare
B : constant String := Buf (First .. Last);
package P is new JWX.JWT (Data => B,

5
src/jwx-stream_auth.ads
View File

@ -18,6 +18,9 @@ is
type Auth_Result_Type is (Auth_OK, Auth_Noent, Auth_Fail, Auth_Invalid);
function Authenticated (Buf : String;
Now : Long_Integer) return Auth_Result_Type;
Now : Long_Integer) return Auth_Result_Type
with
Pre => Buf'Last < Natural'Last - 9 and
Buf'Length > 9;
end JWX.Stream_Auth;

2
src/proof_stream_auth.adb
View File

@ -21,7 +21,7 @@ is
Issuer => "Invalid");
use HA;
begin
OK := Authenticated ("Message", 12345678) = Auth_OK;
OK := Authenticated ("Invalid Message", 12345678) = Auth_OK;
end Test;
end Proof_Stream_Auth;