Skip to content

Commit 3a14ef8

Browse files
jasonpcarrollczjaso
jasonpcarroll
and
czjaso
authored
Fix JSON validation issues concerning missing commas, escaped control characters, and hex escaped 0 value. (#179)
* Fix array parsing to reject missing commas between elements * Fix collection parsing to reject missing commas between elements * Fix escape sequence parsing to reject invalid control character escapes * Allow \u0000 escape sequences in JSON strings * Fix unit tests and skipOneHexEscape logic for overflows. * Fix coverage. * Fix coverage workflow. * Increase complexity threshold, set formatting to check to run on ubuntu-latest. * Update CBMC proofs. --------- Co-authored-by: czjaso <[email protected]>
1 parent 03a463f commit 3a14ef8

File tree

6 files changed

+71
-77
lines changed

6 files changed

+71
-77
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ jobs:
2929
run: |
3030
make -C build/ coverage
3131
declare -a EXCLUDE=("\*test\*" "\*CMakeCCompilerId\*" "\*mocks\*" "\*source\*")
32-
echo ${EXCLUDE[@]} | xargs lcov --rc lcov_branch_coverage=1 -r build/coverage.info -o build/coverage.info
32+
echo ${EXCLUDE[@]} | xargs lcov --rc lcov_branch_coverage=1 --ignore-errors unused -r build/coverage.info -o build/coverage.info
3333
lcov --rc lcov_branch_coverage=1 --list build/coverage.info
3434
- name: Check Coverage
3535
uses: FreeRTOS/CI-CD-Github-Actions/coverage-cop@main
@@ -44,7 +44,7 @@ jobs:
4444
uses: FreeRTOS/CI-CD-Github-Actions/complexity@main
4545
with:
4646
path: ./
47-
horrid_threshold: 12
47+
horrid_threshold: 14
4848

4949
doxygen:
5050
runs-on: ubuntu-latest
@@ -66,7 +66,7 @@ jobs:
6666
path: ./
6767

6868
formatting:
69-
runs-on: ubuntu-20.04
69+
runs-on: ubuntu-latest
7070
steps:
7171
- uses: actions/checkout@v3
7272
- name: Check formatting

‎loop_invariants.patch‎

Lines changed: 37 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
diff --git a/source/core_json.c b/source/core_json.c
2-
index d8694f0..761c44b 100644
2+
index a01c393..ad48f28 100644
33
--- a/source/core_json.c
44
+++ b/source/core_json.c
55
@@ -63,6 +63,21 @@ typedef union
66
#define isCurlyOpen_( x ) ( ( x ) == '{' )
77
#define isCurlyClose_( x ) ( ( x ) == '}' )
8-
8+
99
+/**
1010
+ * Renaming all loop-contract clauses from CBMC for readability.
1111
+ * For more information about loop contracts in CBMC, see
@@ -26,7 +26,7 @@ index d8694f0..761c44b 100644
2626
*
2727
@@ -79,6 +94,9 @@ static void skipSpace( const char * buf,
2828
coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
29-
29+
3030
for( i = *start; i < max; i++ )
3131
+ assigns( i )
3232
+ loopInvariant( *start <= i && i <= max )
@@ -36,7 +36,7 @@ index d8694f0..761c44b 100644
3636
{
3737
@@ -103,6 +121,13 @@ static size_t countHighBits( uint8_t c )
3838
size_t i = 0;
39-
39+
4040
while( ( n & 0x80U ) != 0U )
4141
+ assigns( i, n )
4242
+ loopInvariant (
@@ -61,9 +61,9 @@ index d8694f0..761c44b 100644
6161
+ decreases( j )
6262
{
6363
i++;
64-
65-
@@ -346,6 +378,12 @@ static bool skipOneHexEscape( const char * buf,
66-
if( ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
64+
65+
@@ -343,6 +375,12 @@ static bool skipOneHexEscape( const char * buf,
66+
if( ( end > i ) && ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
6767
{
6868
for( i += 2U; i < end; i++ )
6969
+ assigns( value, i )
@@ -74,50 +74,50 @@ index d8694f0..761c44b 100644
7474
+ decreases( end - i )
7575
{
7676
uint8_t n = hexToInt( buf[ i ] );
77-
78-
@@ -523,6 +561,9 @@ static bool skipString( const char * buf,
77+
78+
@@ -505,6 +543,9 @@ static bool skipString( const char * buf,
7979
i++;
80-
80+
8181
while( i < max )
8282
+ assigns( i )
8383
+ loopInvariant( *start + 1U <= i && i <= max )
8484
+ decreases( max - i )
8585
{
8686
if( buf[ i ] == '"' )
8787
{
88-
@@ -581,6 +622,9 @@ static bool strnEq( const char * a,
88+
@@ -563,6 +604,9 @@ static bool strnEq( const char * a,
8989
coreJSON_ASSERT( ( a != NULL ) && ( b != NULL ) );
90-
90+
9191
for( i = 0; i < n; i++ )
9292
+ assigns( i )
9393
+ loopInvariant( i <= n )
9494
+ decreases( n - i )
9595
{
9696
if( a[ i ] != b[ i ] )
9797
{
98-
@@ -696,6 +740,9 @@ static bool skipDigits( const char * buf,
98+
@@ -678,6 +722,9 @@ static bool skipDigits( const char * buf,
9999
saveStart = *start;
100-
100+
101101
for( i = *start; i < max; i++ )
102102
+ assigns( value, i )
103103
+ loopInvariant( *start <= i && i <= max )
104104
+ decreases( max - i )
105105
{
106106
if( !isdigit_( buf[ i ] ) )
107107
{
108-
@@ -945,6 +992,9 @@ static void skipArrayScalars( const char * buf,
108+
@@ -928,6 +975,9 @@ static bool skipArrayScalars( const char * buf,
109109
i = *start;
110-
110+
111111
while( i < max )
112112
+ assigns( i )
113113
+ loopInvariant( *start <= i && i <= max )
114114
+ decreases( max - i )
115115
{
116116
if( skipAnyScalar( buf, &i, max ) != true )
117117
{
118-
@@ -991,6 +1041,13 @@ static bool skipObjectScalars( const char * buf,
118+
@@ -982,6 +1032,13 @@ static bool skipObjectScalars( const char * buf,
119119
i = *start;
120-
120+
121121
while( i < max )
122122
+ assigns( i, *start, comma )
123123
+ loopInvariant(
@@ -129,11 +129,11 @@ index d8694f0..761c44b 100644
129129
{
130130
if( skipString( buf, &i, max ) != true )
131131
{
132-
@@ -1118,6 +1175,14 @@ static JSONStatus_t skipCollection( const char * buf,
132+
@@ -1109,6 +1166,14 @@ static JSONStatus_t skipCollection( const char * buf,
133133
i = *start;
134-
134+
135135
while( i < max )
136-
+ assigns( i, depth, c, __CPROVER_object_whole( stack ), ret )
136+
+ assigns( i, depth, c, ret, __CPROVER_object_whole( stack ) )
137137
+ loopInvariant(
138138
+ -1 <= depth && depth <= JSON_MAX_DEPTH
139139
+ && *start <= i && i <= max
@@ -144,27 +144,35 @@ index d8694f0..761c44b 100644
144144
{
145145
c = buf[ i ];
146146
i++;
147-
@@ -1407,6 +1472,9 @@ static bool objectSearch( const char * buf,
147+
@@ -1144,6 +1209,7 @@ static JSONStatus_t skipCollection( const char * buf,
148+
149+
if( skipSpaceAndComma( buf, &i, max ) == true )
150+
{
151+
+ __CPROVER_assume( isOpenBracket_(stack[depth]));
152+
if( skipScalars( buf, &i, max, stack[ depth ] ) != true )
153+
{
154+
ret = JSONIllegalDocument;
155+
@@ -1406,6 +1472,9 @@ static bool objectSearch( const char * buf,
148156
skipSpace( buf, &i, max );
149-
157+
150158
while( i < max )
151159
+ assigns( i, key, keyLength, value, valueLength )
152160
+ loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max )
153161
+ decreases( max - i )
154162
{
155163
if( nextKeyValuePair( buf, &i, max, &key, &keyLength,
156164
&value, &valueLength ) != true )
157-
@@ -1474,6 +1542,9 @@ static bool arraySearch( const char * buf,
165+
@@ -1473,6 +1542,9 @@ static bool arraySearch( const char * buf,
158166
skipSpace( buf, &i, max );
159-
167+
160168
while( i < max )
161169
+ assigns( i, currentIndex, value, valueLength )
162170
+ loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max && currentIndex < i )
163171
+ decreases( max - i )
164172
{
165173
if( nextValue( buf, &i, max, &value, &valueLength ) != true )
166174
{
167-
@@ -1539,6 +1610,9 @@ static bool skipQueryPart( const char * buf,
175+
@@ -1538,6 +1610,9 @@ static bool skipQueryPart( const char * buf,
168176
while( ( i < max ) &&
169177
!isSeparator_( buf[ i ] ) &&
170178
!isSquareOpen_( buf[ i ] ) )
@@ -174,9 +182,9 @@ index d8694f0..761c44b 100644
174182
{
175183
i++;
176184
}
177-
@@ -1585,6 +1659,17 @@ static JSONStatus_t multiSearch( const char * buf,
185+
@@ -1584,6 +1659,17 @@ static JSONStatus_t multiSearch( const char * buf,
178186
coreJSON_ASSERT( ( max > 0U ) && ( queryLength > 0U ) );
179-
187+
180188
while( i < queryLength )
181189
+ assigns( i, start, queryStart, value, length )
182190
+ loopInvariant(
@@ -191,4 +199,4 @@ index d8694f0..761c44b 100644
191199
+ decreases( queryLength - i )
192200
{
193201
bool found = false;
194-
202+

‎source/core_json.c‎

Lines changed: 25 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -321,8 +321,6 @@ static uint8_t hexToInt( char c )
321321
*
322322
* @return true if a valid escape sequence was present;
323323
* false otherwise.
324-
*
325-
* @note For the sake of security, \u0000 is disallowed.
326324
*/
327325
static bool skipOneHexEscape( const char * buf,
328326
size_t * start,
@@ -333,17 +331,16 @@ static bool skipOneHexEscape( const char * buf,
333331
size_t i = 0U, end = 0U;
334332
uint16_t value = 0U;
335333

336-
coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
337-
coreJSON_ASSERT( outValue != NULL );
334+
coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) && ( outValue != NULL ) );
338335

339336
i = *start;
340337
#define HEX_ESCAPE_LENGTH ( 6U ) /* e.g., \u1234 */
341338
/* MISRA Ref 14.3.1 [Configuration dependent invariant] */
342339
/* More details at: https://github.com/FreeRTOS/coreJSON/blob/main/MISRA.md#rule-143 */
343340
/* coverity[misra_c_2012_rule_14_3_violation] */
344-
end = ( i <= ( SIZE_MAX - HEX_ESCAPE_LENGTH ) ) ? ( i + HEX_ESCAPE_LENGTH ) : SIZE_MAX;
341+
end = i + HEX_ESCAPE_LENGTH;
345342

346-
if( ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
343+
if( ( end > i ) && ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
347344
{
348345
for( i += 2U; i < end; i++ )
349346
{
@@ -358,7 +355,7 @@ static bool skipOneHexEscape( const char * buf,
358355
}
359356
}
360357

361-
if( ( i == end ) && ( value > 0U ) )
358+
if( i == end )
362359
{
363360
ret = true;
364361
*outValue = value;
@@ -382,8 +379,6 @@ static bool skipOneHexEscape( const char * buf,
382379
*
383380
* @return true if a valid escape sequence was present;
384381
* false otherwise.
385-
*
386-
* @note For the sake of security, \u0000 is disallowed.
387382
*/
388383
#define isHighSurrogate( x ) ( ( ( x ) >= 0xD800U ) && ( ( x ) <= 0xDBFFU ) )
389384
#define isLowSurrogate( x ) ( ( ( x ) >= 0xDC00U ) && ( ( x ) <= 0xDFFFU ) )
@@ -437,8 +432,6 @@ static bool skipHexEscape( const char * buf,
437432
*
438433
* @return true if a valid escape sequence was present;
439434
* false otherwise.
440-
*
441-
* @note For the sake of security, \NUL is disallowed.
442435
*/
443436
static bool skipEscape( const char * buf,
444437
size_t * start,
@@ -457,9 +450,6 @@ static bool skipEscape( const char * buf,
457450

458451
switch( c )
459452
{
460-
case '\0':
461-
break;
462-
463453
case 'u':
464454
ret = skipHexEscape( buf, &i, max );
465455
break;
@@ -477,14 +467,6 @@ static bool skipEscape( const char * buf,
477467
break;
478468

479469
default:
480-
481-
/* a control character: (NUL,SPACE) */
482-
if( iscntrl_( c ) )
483-
{
484-
i += 2U;
485-
ret = true;
486-
}
487-
488470
break;
489471
}
490472
}
@@ -934,11 +916,12 @@ static bool skipSpaceAndComma( const char * buf,
934916
*
935917
* @note Stops advance if a value is an object or array.
936918
*/
937-
static void skipArrayScalars( const char * buf,
919+
static bool skipArrayScalars( const char * buf,
938920
size_t * start,
939921
size_t max )
940922
{
941923
size_t i = 0U;
924+
bool ret = true;
942925

943926
coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
944927

@@ -953,11 +936,19 @@ static void skipArrayScalars( const char * buf,
953936

954937
if( skipSpaceAndComma( buf, &i, max ) != true )
955938
{
939+
/* After parsing a scalar, we must either have a comma (followed by more content)
940+
* or be at a closing bracket. If neither, the array is malformed. */
941+
if( ( i >= max ) || !isSquareClose_( buf[ i ] ) )
942+
{
943+
ret = false;
944+
}
945+
956946
break;
957947
}
958948
}
959949

960950
*start = i;
951+
return ret;
961952
}
962953

963954
/**
@@ -1071,7 +1062,7 @@ static bool skipScalars( const char * buf,
10711062
{
10721063
if( !isSquareClose_( buf[ i ] ) )
10731064
{
1074-
skipArrayScalars( buf, start, max );
1065+
ret = skipArrayScalars( buf, start, max );
10751066
}
10761067
}
10771068
else
@@ -1151,14 +1142,22 @@ static JSONStatus_t skipCollection( const char * buf,
11511142
{
11521143
depth--;
11531144

1154-
if( ( skipSpaceAndComma( buf, &i, max ) == true ) &&
1155-
isOpenBracket_( stack[ depth ] ) )
1145+
if( skipSpaceAndComma( buf, &i, max ) == true )
11561146
{
11571147
if( skipScalars( buf, &i, max, stack[ depth ] ) != true )
11581148
{
11591149
ret = JSONIllegalDocument;
11601150
}
11611151
}
1152+
else
1153+
{
1154+
/* After closing a nested collection, if there is no comma found when calling
1155+
* skipSpaceAndComma, then we must be at the end of the parent collection. */
1156+
if( ( i < max ) && !isMatchingBracket_( stack[ depth ], buf[ i ] ) )
1157+
{
1158+
ret = JSONIllegalDocument;
1159+
}
1160+
}
11621161

11631162
break;
11641163
}

‎test/cbmc/proofs/JSON_Validate/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,5 +12,6 @@ USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
1212

1313
USE_FUNCTION_CONTRACTS += skipAnyScalar
1414
USE_FUNCTION_CONTRACTS += skipCollection
15+
USE_FUNCTION_CONTRACTS += skipSpace
1516

1617
include ../Makefile-json.common

0 commit comments

Comments
 (0)