verifier.js

const fs = require('fs');
const { XMLParser } = require('fast-xml-parser');
const acorn = require('acorn');
const walk = require('acorn-walk');

const FILE_PATH = process.argv[2];
if (!FILE_PATH) {
    console.error("Usage: node verifier.js <path_to_xml>");
    process.exit(1);
}

function main() {
    const xmlData = fs.readFileSync(FILE_PATH, 'utf8');
    const parser = new XMLParser({ ignoreAttributes: false, attributeNamePrefix: "@_" });
    const jsonObj = parser.parse(xmlData);

    const updates = findUpdates(jsonObj);

    // STRICTER FIND: Only look for the Resource which contains the script
    const relevantUpdate = updates.find(u =>
        u.type === 'Scripted REST Resource'
    );

    if (!relevantUpdate) {
        console.error("No relevant Scripted REST Resource found.");
        process.exit(0);
    }

    // EXTRACT METADATA
    const action = relevantUpdate.action || "UNKNOWN";

    const innerParser = new XMLParser({ ignoreAttributes: false, attributeNamePrefix: "@_" });
    const payloadObj = innerParser.parse(relevantUpdate.payload);

    let table = "UNKNOWN";
    if (payloadObj.record_update && payloadObj.record_update["@_table"]) {
        table = payloadObj.record_update["@_table"];
    }

    let script = "";
    try {
        script = payloadObj.record_update.sys_ws_operation.operation_script;
    } catch (e) {
        // missing script
    }

    script = decodeEntities(script);
    console.warn("DEBUG: Analyzing script content length: " + script.length);
    const taintAnalysis = analyzeScript(script);

    // Generate SMT2
    console.log(`;; MODEL: Auto-generated from ${FILE_PATH}`);
    console.log(`(assert (= Action "${action}"))`);
    console.log(`(assert (= Table "${table}"))`);
    console.log(`(assert (= script_source_is_user_input ${taintAnalysis.hasSource}))`);
    console.log(`(assert (= script_sink_is_dangerous ${taintAnalysis.hasSink}))`);
    console.log(`(assert (= script_flow_exists ${taintAnalysis.hasFlow}))`);
}

function findUpdates(jsonObj) {
    if (jsonObj.unload && jsonObj.unload.sys_update_xml) {
        const updateXml = jsonObj.unload.sys_update_xml;
        return Array.isArray(updateXml) ? updateXml : [updateXml];
    }
    return [];
}

function analyzeScript(scriptContent) {
    if (!scriptContent) return { hasSource: false, hasSink: false, hasFlow: false };

    let ast;
    try {
        ast = acorn.parse(scriptContent, { ecmaVersion: 2020 });
    } catch (e) {
        console.warn("Script parsing failed: " + e.message);
        return { hasSource: false, hasSink: false, hasFlow: false };
    }

    let taintedVars = new Set();
    let hasSource = false;
    let hasSink = false;
    let hasFlow = false;

    walk.simple(ast, {
        VariableDeclarator(node) {
            if (node.init) {
                if (isSource(node.init, taintedVars)) {
                    hasSource = true;
                    if (node.id.type === 'Identifier') {
                        taintedVars.add(node.id.name);
                    }
                }
            }
        },
        AssignmentExpression(node) {
            if (isSource(node.right, taintedVars)) {
                hasSource = true;
                if (node.left.type === 'Identifier') {
                    taintedVars.add(node.left.name);
                }
            }
        },
        CallExpression(node) {
            if (node.callee.name === 'eval') {
                node.arguments.forEach(arg => {
                    if (arg.type === 'Identifier' && taintedVars.has(arg.name)) {
                        hasSink = true;
                        hasFlow = true;
                    }
                });
            }
            if (node.callee.type === 'MemberExpression' && node.callee.property.name === 'evaluateScript') {
                if (node.arguments.length >= 2) {
                    const scriptArg = node.arguments[1];
                    if (scriptArg.type === 'Identifier' && taintedVars.has(scriptArg.name)) {
                        hasSink = true;
                        hasFlow = true;
                    }
                    if (scriptArg.type === 'MemberExpression') {
                        let flat = flattenMemberExpression(scriptArg);
                        const parts = flat.split('.');
                        if (taintedVars.has(parts[0])) {
                            hasSink = true;
                            hasFlow = true;
                        }
                    }
                }
            }
        }
    });

    return { hasSource, hasSink, hasFlow };
}

function isSource(node, taintedVars) {
    const chain = flattenMemberExpression(node);
    if (chain.startsWith("request.body")) return true;
    if (chain.startsWith("request.queryParams")) return true;
    if (node.type === 'Identifier' && taintedVars.has(node.name)) {
        return true;
    }
    return false;
}

function flattenMemberExpression(node) {
    if (node.type === 'MemberExpression') {
        const object = flattenMemberExpression(node.object);
        const property = node.property.name || '';
        return `${object}.${property}`;
    } else if (node.type === 'Identifier') {
        return node.name;
    }
    return '';
}

function decodeEntities(encodedString) {
    if (!encodedString) return "";
    return encodedString.replace(/&#(\d+);/g, function (match, dec) {
        return String.fromCharCode(dec);
    }).replace(/&quot;/g, '"')
        .replace(/&apos;/g, "'")
        .replace(/&lt;/g, '<')
        .replace(/&gt;/g, '>')
        .replace(/&amp;/g, '&');
}

main();